1  /-
  2  Copyright (c) 2018 Johannes Hölzl. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Authors: Johannes Hölzl, Jens Wagemaker
  5  
  6  GCD domain and integral domains with normalization functions
  7  
  8  TODO: abstract the domains to to semi domains (i.e. domains on semirings) to include ℕ and ℕ[X] etc.
  9  -/
 10  import algebra.associated data.int.gcd
src         └────────────────┘ └──────────┘
 11  
 12  variables {α : Type*}
 13  
 14  set_option old_structure_cmd true
doc             └───────────────┘
 15  
 16  
 17  
 18  section prio
 19  set_option default_priority 100 -- see Note [default priority]
doc             └──────────────┘
 20  /-- Normalization domain: multiplying with `norm_unit` gives a normal form for associated elements. -/
 21  class normalization_domain (α : Type*) extends integral_domain α :=
id                                  └───┘          └─────────────┘ 
src                                                 └─────────────┘
typ                                 └───┘          └─────────────┘ 
 22  (norm_unit : α → units α)
id                  └───┘ 
src                   └───┘
typ                 └───┘ 
 23  (norm_unit_zero      : norm_unit 0 = 1)
id                          └───────┘   
src                                     
typ                         └───────┘   
 24  (norm_unit_mul       : ∀{a b}, a ≠ 0 → b ≠ 0 → norm_unit (a * b) = norm_unit a * norm_unit b)
id                                           └───────┘       └───────┘   └───────┘ 
src                                                                             
typ                                          └───────┘       └───────┘   └───────┘ 
 25  (norm_unit_coe_units : ∀(u : units α), norm_unit u = u⁻¹)
id                               └───┘    └───────┘   └┘
src                               └───┘                   └┘
typ                              └───┘    └───────┘   └┘
 26  end prio
 27  
 28  export normalization_domain (norm_unit norm_unit_zero norm_unit_mul norm_unit_coe_units)
 29  
 30  attribute [simp] norm_unit_coe_units norm_unit_zero norm_unit_mul
id                    └─────────────────┘ └────────────┘ └───────────┘
src                   └─────────────────┘ └────────────┘ └───────────┘
typ                   └─────────────────┘ └────────────┘ └───────────┘
doc             └──┘
 31  
 32  section normalization_domain
 33  variable [normalization_domain α]
id             └──────────────────┘
src            └──────────────────┘
typ            └──────────────────┘
doc            └──────────────────┘
 34  
 35  def normalize (x : α) : α :=
id                          
typ                         
 36  x * norm_unit x
id     └───────┘ 
src     └───────┘
typ    └───────┘ 
 37  
 38  theorem associated_normalize {x : α} : associated x (normalize x) :=
id                                         └────────┘   └───────┘ 
src                                         └────────┘    └───────┘
typ                                        └────────┘   └───────┘ 
 39  ⟨_, rfl⟩
id       └─┘
src      └─┘
typ      └─┘
 40  
 41  theorem normalize_associated {x : α} : associated (normalize x) x :=
id                                         └────────┘  └───────┘   
src                                         └────────┘  └───────┘
typ                                        └────────┘  └───────┘   
 42  associated_normalize.symm
id   └──────────────────┘└───┘
src  └──────────────────┘└───┘
typ  └──────────────────┘└───┘
 43  
 44  @[simp] theorem norm_unit_one : norm_unit (1:α) = 1 :=
id                                   └───────┘      
src                                  └───────┘       
typ                                  └───────┘      
doc    └──┘
 45  norm_unit_coe_units 1
id   └─────────────────┘
src  └─────────────────┘
typ  └─────────────────┘
 46  
 47  @[simp] lemma normalize_zero : normalize (0 : α) = 0 :=
id                                  └───────┘        
src                                 └───────┘         
typ                                 └───────┘        
doc    └──┘
 48  by rw [normalize, zero_mul]
id          └───────┘  └──────┘
src     └──┘└───────┘└┘└──────┘└─
typ     └──┘└───────┘└┘└──────┘└─
doc     └──┘         └┘        └─
txt     └──┘         └┘        └─
par     └──┘         └┘        └─
pid       └┘         └┘        
st     └────────────┘└────────┘
 49  
src  
typ  
doc  
txt  
par  
pid  
st   
 50  @[simp] lemma normalize_one : normalize (1 : α) = 1 :=
id                                 └───────┘        
src                                └───────┘         
typ                                └───────┘        
doc    └──┘
 51  by rw [normalize, norm_unit_one, units.coe_one, mul_one]
id          └───────┘  └───────────┘  └───────────┘  └─────┘
src     └──┘└───────┘└┘└───────────┘└┘└───────────┘└┘└─────┘└─
typ     └──┘└───────┘└┘└───────────┘└┘└───────────┘└┘└─────┘└─
doc     └──┘         └┘             └┘             └┘       └─
txt     └──┘         └┘             └┘             └┘       └─
par     └──┘         └┘             └┘             └┘       └─
pid       └┘         └┘             └┘             └┘       
st     └────────────┘└─────────────┘└─────────────┘└───────┘
 52  
src  
typ  
doc  
txt  
par  
pid  
st   
 53  lemma normalize_coe_units (u : units α) : normalize (u : α) = 1 :=
id                                  └───┘     └───────┘       
src                                 └───┘      └───────┘         
typ                                 └───┘     └───────┘       
 54  by rw [normalize, norm_unit_coe_units, ← units.coe_mul, mul_inv_self, units.coe_one]
id          └───────┘  └─────────────────┘    └───────────┘  └──────────┘  └───────────┘
src     └──┘└───────┘└┘└─────────────────┘└──┘└───────────┘└┘└──────────┘└┘└───────────┘└─
typ     └──┘└───────┘└┘└─────────────────┘└──┘└───────────┘└┘└──────────┘└┘└───────────┘└─
doc     └──┘         └┘                   └──┘             └┘            └┘             └─
txt     └──┘         └┘                   └──┘             └┘            └┘             └─
par     └──┘         └┘                   └──┘             └┘            └┘             └─
pid       └┘         └┘                   └──┘             └┘            └┘             
st     └────────────┘└───────────────────┘└───────────────┘└────────────┘└─────────────┘
 55  
src  
typ  
doc  
txt  
par  
pid  
st   
 56  theorem normalize_mul (x y : α) : normalize (x * y) = normalize x * normalize y :=
id                                    └───────┘       └───────┘   └───────┘ 
src                                    └───────┘         └───────┘    └───────┘
typ                                   └───────┘       └───────┘   └───────┘ 
 57  classical.by_cases (λ hx : x = 0, by rw [hx, zero_mul, normalize_zero, zero_mul]) $ λ hx,
id   └────────────────┘                     └┘  └──────┘  └────────────┘  └──────┘       └┘
src  └────────────────┘                  └──┘  └┘└──────┘└┘└────────────┘└┘└──────┘
typ  └────────────────┘                 └──┘└┘└┘└──────┘└┘└────────────┘└┘└──────┘      └┘
doc                                       └──┘  └┘        └┘              └┘        
txt                                       └──┘  └┘        └┘              └┘        
par                                       └──┘  └┘        └┘              └┘        
pid                                         └┘  └┘        └┘              └┘        
st                                       └─────┘└────────┘└──────────────┘└────────┘
 58  classical.by_cases (λ hy : y = 0, by rw [hy, mul_zero, normalize_zero, mul_zero]) $ λ hy,
id   └────────────────┘                     └┘  └──────┘  └────────────┘  └──────┘       └┘
src  └────────────────┘                  └──┘  └┘└──────┘└┘└────────────┘└┘└──────┘
typ  └────────────────┘                 └──┘└┘└┘└──────┘└┘└────────────┘└┘└──────┘      └┘
doc                                       └──┘  └┘        └┘              └┘        
txt                                       └──┘  └┘        └┘              └┘        
par                                       └──┘  └┘        └┘              └┘        
pid                                         └┘  └┘        └┘              └┘        
st                                       └─────┘└────────┘└──────────────┘└────────┘
 59  by simp only [normalize, norm_unit_mul hx hy, units.coe_mul]; simp only [mul_assoc, mul_left_comm y]
id                 └───────┘  └───────────┘ └┘ └┘  └───────────┘              └───────┘  └───────────┘ 
src     └─────────┘└───────┘└┘└───────────┘    └┘└───────────┘  └─────────┘└───────┘└┘└───────────┘ └─
typ     └─────────┘└───────┘└┘└───────────┘└┘└┘└┘└───────────┘  └─────────┘└───────┘└┘└───────────┘└─
doc     └─────────┘         └┘                 └┘               └─────────┘         └┘              └─
txt     └─────────┘         └┘                 └┘               └─────────┘         └┘              └─
par     └─────────┘         └┘                 └┘               └─────────┘         └┘              └─
pid         └──┘└┘         └┘                 └┘                   └──┘└┘         └┘              
st     └──────────────────────────────────────────────────────────────────────────────────────────────────
 60  
src  
typ  
doc  
txt  
par  
pid  
st   
 61  lemma normalize_eq_zero {x : α} : normalize x = 0 ↔ x = 0 :=
id                                    └───────┘       
src                                    └───────┘         
typ                                   └───────┘       
 62  ⟨λ hx, (associated_zero_iff_eq_zero x).1 $ hx ▸ associated_normalize, by rintro rfl; exact normalize_zero⟩
id      └┘   └─────────────────────────┘      └┘  └──────────────────┘                       └────────────┘
src          └─────────────────────────┘           └──────────────────┘     └────────┘  └────┘└────────────┘
typ     └┘   └─────────────────────────┘      └┘  └──────────────────┘     └────────┘  └────┘└────────────┘
doc                                                                           └────────┘  └────┘
txt                                                                           └────────┘  └────┘
par                                                                           └────────┘  └────┘
pid                                                                                 └──┘       
st                                                                           └───────────────────────────────┘
 63  
 64  lemma normalize_eq_one {x : α} : normalize x = 1 ↔ is_unit x :=
id                                   └───────┘      └─────┘ 
src                                   └───────┘       └─────┘
typ                                  └───────┘      └─────┘ 
doc                                                     └─────┘
 65  ⟨λ hx, is_unit_iff_exists_inv.2 ⟨_, hx⟩, λ ⟨u, hu⟩, hu.symm ▸ normalize_coe_units u⟩
id      └┘  └────────────────────┘      └┘       └┘     └───┘  └─────────────────┘
src         └────────────────────┘                        └───┘  └─────────────────┘
typ     └┘  └────────────────────┘      └┘       └┘     └───┘  └─────────────────┘
 66  
 67  theorem norm_unit_mul_norm_unit (a : α) : norm_unit (a * norm_unit a) = 1 :=
id                                            └───────┘    └───────┘   
src                                            └───────┘     └───────┘    
typ                                           └───────┘    └───────┘   
 68  classical.by_cases (assume : a = 0, by simp only [this, norm_unit_zero, zero_mul]) $
id   └────────────────┘                              └──┘  └────────────┘  └──────┘
src  └────────────────┘                    └─────────┘    └┘└────────────┘└┘└──────┘
typ  └────────────────┘                   └─────────┘└──┘└┘└────────────┘└┘└──────┘
doc                                         └─────────┘    └┘              └┘        
txt                                         └─────────┘    └┘              └┘        
par                                         └─────────┘    └┘              └┘        
pid                                             └──┘└┘    └┘              └┘        
st                                         └─────────────────────────────────────────┘
 69    assume h, by rw [norm_unit_mul h (units.ne_zero _), norm_unit_coe_units, mul_inv_eq_one]
id                     └───────────┘   └───────────┘     └─────────────────┘  └────────────┘
src                 └──┘└───────────┘  └───────────┘└───┘└─────────────────┘└┘└────────────┘└─
typ                └──┘└───────────┘ └───────────┘└───┘└─────────────────┘└┘└────────────┘└─
doc                 └──┘               └───────────┘└───┘                   └┘              └─
txt                 └──┘                            └───┘                   └┘              └─
par                 └──┘                            └───┘                   └┘              └─
pid                   └┘                            └───┘                   └┘              
st                 └────────────────────────────────────┘└───────────────────┘└──────────────┘
 70  
src  
typ  
doc  
txt  
par  
pid  
st   
 71  theorem normalize_idem (x : α) : normalize (normalize x) = normalize x :=
id                                   └───────┘  └───────┘    └───────┘ 
src                                   └───────┘  └───────┘     └───────┘
typ                                  └───────┘  └───────┘    └───────┘ 
 72  by rw [normalize, normalize, norm_unit_mul_norm_unit, units.coe_one, mul_one]
id          └───────┘  └───────┘  └─────────────────────┘  └───────────┘  └─────┘
src     └──┘└───────┘└┘└───────┘└┘└─────────────────────┘└┘└───────────┘└┘└─────┘└─
typ     └──┘└───────┘└┘└───────┘└┘└─────────────────────┘└┘└───────────┘└┘└─────┘└─
doc     └──┘         └┘         └┘                       └┘             └┘       └─
txt     └──┘         └┘         └┘                       └┘             └┘       └─
par     └──┘         └┘         └┘                       └┘             └┘       └─
pid       └┘         └┘         └┘                       └┘             └┘       
st     └────────────┘└─────────┘└───────────────────────┘└─────────────┘└───────┘
 73  
src  
typ  
doc  
txt  
par  
pid  
st   
 74  theorem normalize_eq_normalize {a b : α}
id                                         
typ                                        
 75    (hab : a ∣ b) (hba : b ∣ a) : normalize a = normalize b :=
id                             └───────┘   └───────┘ 
src                                └───────┘    └───────┘
typ                            └───────┘   └───────┘ 
 76  begin
st   └─────
 77    rcases associated_of_dvd_dvd hab hba with ⟨u, rfl⟩,
id            └───────────────────┘ └─┘ └─┘
src    └─────┘└───────────────────┘      └────────────┘
typ    └─────┘└───────────────────┘└─┘└─┘└────────────┘
doc    └─────┘                           └────────────┘
txt    └─────┘                           └────────────┘
par    └─────┘                           └────────────┘
pid                                     └────────────┘
st   ───────────────────────────────────────────────────┘└─
 78    refine classical.by_cases (by rintro rfl; simp only [zero_mul]) (assume ha : a ≠ 0, _),
id            └────────────────┘                            └──────┘                 
src    └─────┘└────────────────┘   └────────┘└┘└─────────┘└──────┘└┘       └────┘ └────┘
typ    └─────┘└────────────────┘   └────────┘└┘└─────────┘└──────┘└┘       └────┘└────┘
doc    └─────┘                     └────────┘└┘└─────────┘        └┘       └────┘  └────┘
txt    └─────┘                     └────────┘└┘└─────────┘        └┘       └────┘  └────┘
par    └─────┘                     └────────┘└┘└─────────┘        └┘       └────┘  └────┘
pid                               └──────────────────────┘        └─┘       └────┘  └────┘
st   ──────────────────────────────┘└───────────────────────────────┘└──────────────────────┘└─
 79    suffices : a * ↑(norm_unit a) = a * ↑u * ↑(norm_unit a) * ↑u⁻¹,
id                                             └───────┘      └┘
src    └─────────┘            └┘       └───────┘ └┘   └┘
typ    └─────────┘            └┘       └───────┘└┘  └┘
doc    └─────────┘              └┘                  └┘ 
txt    └─────────┘              └┘                  └┘ 
par    └─────────┘              └┘                  └┘ 
pid    └───────┘└┘              └┘                  └┘ 
st   ───────────────────────────────────────────────────────────────┘
 80      by simpa only [normalize, mul_assoc, norm_unit_mul ha u.ne_zero, norm_unit_coe_units],
id                      └───────┘  └───────┘  └───────────┘ └┘ └───────┘  └─────────────────┘
src         └──────────┘└───────┘└┘└───────┘└┘└───────────┘  └───────┘└┘└─────────────────┘
typ         └──────────┘└───────┘└┘└───────┘└┘└───────────┘└┘└───────┘└┘└─────────────────┘
doc         └──────────┘         └┘         └┘               └───────┘└┘                   
txt         └──────────┘         └┘         └┘                        └┘                   
par         └──────────┘         └┘         └┘                        └┘                   
pid              └──┘└┘         └┘         └┘                        └┘                   
st                                                                                            └─
 81    calc a * ↑(norm_unit a) = a * ↑(norm_unit a) * ↑u * ↑u⁻¹:
id     └──┘
src    └──┘
typ    └──┘
doc    └──┘
st   ────────────────────────────────────────────────────────────
 82        (units.mul_inv_cancel_right _ _).symm
id          └────────────────────────┘     └──┘
src         └────────────────────────┘     └──┘
typ         └────────────────────────┘     └──┘
st   ────────────────────────────────────────────
 83      ... = a * ↑u * ↑(norm_unit a) * ↑u⁻¹ : by rw mul_right_comm a
id                        └───────┘                 └────────────┘ 
src                       └───────┘                └─┘└────────────┘ 
typ                       └───────┘              └─┘└────────────┘
doc                                                └─┘               
txt                                                └─┘               
par                                                └─┘               
pid                                                                 
st   ────────────────────────────────────────────┘└───────────────────┘
 84  end
st   └─┘
 85  
 86  lemma normalize_eq_normalize_iff {x y : α} : normalize x = normalize y ↔ x ∣ y ∧ y ∣ x :=
id                                               └───────┘   └───────┘         
src                                               └───────┘    └───────┘            
typ                                              └───────┘   └───────┘         
 87  ⟨λ h, ⟨dvd_mul_unit_iff.1 ⟨_, h.symm⟩, dvd_mul_unit_iff.1 ⟨_, h⟩⟩,
id         └──────────────┘      └───┘   └──────────────┘      
src         └──────────────┘       └───┘   └──────────────┘
typ        └──────────────┘      └───┘   └──────────────┘      
 88  λ ⟨hxy, hyx⟩, normalize_eq_normalize hxy hyx⟩
id     └─┘  └─┘   └────────────────────┘
src                └────────────────────┘
typ    └─┘  └─┘   └────────────────────┘
 89  
 90  theorem dvd_antisymm_of_normalize_eq {a b : α}
id                                               
typ                                              
 91    (ha : normalize a = a) (hb : normalize b = b) (hab : a ∣ b) (hba : b ∣ a) :
id           └───────┘           └───────┘                         
src          └───────┘             └───────┘                             
typ          └───────┘           └───────┘                         
 92    a = b :=
id       
src      
typ      
 93  ha ▸ hb ▸ normalize_eq_normalize hab hba
id   └┘  └┘  └────────────────────┘ └─┘ └─┘
src          └────────────────────┘
typ  └┘  └┘  └────────────────────┘ └─┘ └─┘
 94  
 95  @[simp] lemma dvd_normalize_iff {a b : α} : a ∣ normalize b ↔ a ∣ b :=
id                                                └───────┘     
src                                                 └───────┘      
typ                                               └───────┘     
doc    └──┘
 96  dvd_mul_unit_iff
id   └──────────────┘
src  └──────────────┘
typ  └──────────────┘
 97  
 98  @[simp] lemma normalize_dvd_iff {a b : α} : normalize a ∣ b ↔ a ∣ b :=
id                                              └───────┘       
src                                              └───────┘         
typ                                             └───────┘       
doc    └──┘
 99  mul_unit_dvd_iff
id   └──────────────┘
src  └──────────────┘
typ  └──────────────┘
100  
101  end normalization_domain
102  
103  namespace associates
104  variable [normalization_domain α]
id             └──────────────────┘
src            └──────────────────┘
typ            └──────────────────┘
doc            └──────────────────┘
105  
106  local attribute [instance] associated.setoid
id                              └───────────────┘
src                             └───────────────┘
typ                             └───────────────┘
107  
108  protected def out : associates α → α :=
id                       └────────┘    
src                      └────────┘
typ                      └────────┘    
109  quotient.lift (normalize : α → α) $ λ a b ⟨u, hu⟩, hu ▸
id   └───────────┘  └───────┘                 └┘      
src  └───────────┘  └───────┘                              
typ  └───────────┘  └───────┘                 └┘      
110  normalize_eq_normalize ⟨_, rfl⟩ (mul_unit_dvd_iff.2 $ dvd_refl a)
id   └────────────────────┘     └─┘   └──────────────┘    └──────┘ 
src  └────────────────────┘     └─┘   └──────────────┘    └──────┘
typ  └────────────────────┘     └─┘   └──────────────┘    └──────┘ 
111  
112  lemma out_mk (a : α) : (associates.mk a).out = normalize a := rfl
id                          └───────────┘  └─┘   └───────┘     └─┘
src                          └───────────┘   └─┘   └───────┘      └─┘
typ                         └───────────┘  └─┘   └───────┘     └─┘
113  
114  @[simp] lemma out_one : (1 : associates α).out = 1 :=
id                                └────────┘  └─┘  
src                               └────────┘   └─┘  
typ                               └────────┘  └─┘  
doc    └──┘
115  normalize_one
id   └───────────┘
src  └───────────┘
typ  └───────────┘
116  
117  lemma out_mul (a b : associates α) : (a * b).out = a.out * b.out :=
id                        └────────┘         └─┘   └──┘  └──┘
src                       └────────┘            └─┘    └──┘   └──┘
typ                       └────────┘         └─┘   └──┘  └──┘
118  quotient.induction_on₂ a b $ assume a b,
id   └────────────────────┘             
src  └────────────────────┘
typ  └────────────────────┘             
119  by simp only [associates.quotient_mk_eq_mk, out_mk, mk_mul_mk, normalize_mul]
id                 └──────────────────────────┘  └────┘  └───────┘  └───────────┘
src     └─────────┘└──────────────────────────┘└┘└────┘└┘└───────┘└┘└───────────┘└─
typ     └─────────┘└──────────────────────────┘└┘└────┘└┘└───────┘└┘└───────────┘└─
doc     └─────────┘                            └┘      └┘         └┘             └─
txt     └─────────┘                            └┘      └┘         └┘             └─
par     └─────────┘                            └┘      └┘         └┘             └─
pid         └──┘└┘                            └┘      └┘         └┘             
st     └───────────────────────────────────────────────────────────────────────────
120  
src  
typ  
doc  
txt  
par  
pid  
st   
121  lemma dvd_out_iff (a : α) (b : associates α) : a ∣ b.out ↔ associates.mk a ≤ b :=
id                                 └────────┘       └──┘  └───────────┘   
src                                 └────────┘          └──┘  └───────────┘   
typ                                └────────┘       └──┘  └───────────┘   
122  quotient.induction_on b $ by simp [associates.out_mk, associates.quotient_mk_eq_mk, mk_le_mk_iff_dvd_iff]
id   └───────────────────┘             └───────────────┘  └──────────────────────────┘  └──────────────────┘
src  └───────────────────┘        └────┘└───────────────┘└┘└──────────────────────────┘└┘└──────────────────┘└─
typ  └───────────────────┘       └────┘└───────────────┘└┘└──────────────────────────┘└┘└──────────────────┘└─
doc                               └────┘                 └┘                            └┘                    └─
txt                               └────┘                 └┘                            └┘                    └─
par                               └────┘                 └┘                            └┘                    └─
pid                                                    └┘                            └┘                    
st                               └─────────────────────────────────────────────────────────────────────────────
123  
src  
typ  
doc  
txt  
par  
pid  
st   
124  lemma out_dvd_iff (a : α) (b : associates α) : b.out ∣ a ↔ b ≤ associates.mk a :=
id                                 └────────┘     └──┘      └───────────┘ 
src                                 └────────┘       └──┘        └───────────┘
typ                                └────────┘     └──┘      └───────────┘ 
125  quotient.induction_on b $ by simp [associates.out_mk, associates.quotient_mk_eq_mk, mk_le_mk_iff_dvd_iff]
id   └───────────────────┘             └───────────────┘  └──────────────────────────┘  └──────────────────┘
src  └───────────────────┘        └────┘└───────────────┘└┘└──────────────────────────┘└┘└──────────────────┘└─
typ  └───────────────────┘       └────┘└───────────────┘└┘└──────────────────────────┘└┘└──────────────────┘└─
doc                               └────┘                 └┘                            └┘                    └─
txt                               └────┘                 └┘                            └┘                    └─
par                               └────┘                 └┘                            └┘                    └─
pid                                                    └┘                            └┘                    
st                               └─────────────────────────────────────────────────────────────────────────────
126  
src  
typ  
doc  
txt  
par  
pid  
st   
127  @[simp] lemma out_top : (⊤ : associates α).out = 0 :=
id                               └────────┘  └─┘  
src                              └────────┘   └─┘  
typ                              └────────┘  └─┘  
doc    └──┘
128  normalize_zero
id   └────────────┘
src  └────────────┘
typ  └────────────┘
129  
130  @[simp] lemma normalize_out (a : associates α) : normalize a.out = a.out :=
id                                    └────────┘     └───────┘ └──┘  └──┘
src                                   └────────┘      └───────┘  └──┘   └──┘
typ                                   └────────┘     └───────┘ └──┘  └──┘
doc    └──┘
131  quotient.induction_on a normalize_idem
id   └───────────────────┘  └────────────┘
src  └───────────────────┘   └────────────┘
typ  └───────────────────┘  └────────────┘
132  
133  end associates
134  
135  section prio
136  set_option default_priority 100 -- see Note [default priority]
doc             └──────────────┘
137  /-- GCD domain: an integral domain with normalization and `gcd` (greatest common divisor) and
138  `lcm` (least common multiple) operations. In this setting `gcd` and `lcm` form a bounded lattice on
139  the associated elements where `gcd` is the infimum, `lcm` is the supremum, `1` is bottom, and
140  `0` is top. The type class focuses on `gcd` and we derive the correpsonding `lcm` facts from `gcd`.
141  -/
142  class gcd_domain (α : Type*) extends normalization_domain α :=
id                        └───┘          └──────────────────┘ 
src                                       └──────────────────┘
typ                       └───┘          └──────────────────┘ 
doc                                       └──────────────────┘
143  (gcd : α → α → α)
id               
typ              
144  (lcm : α → α → α)
id               
typ              
145  (gcd_dvd_left   : ∀a b, gcd a b ∣ a)
id                         └─┘    
src                                  
typ                        └─┘    
146  (gcd_dvd_right  : ∀a b, gcd a b ∣ b)
id                         └─┘    
src                                  
typ                        └─┘    
147  (dvd_gcd        : ∀{a b c}, a ∣ c → a ∣ b → a ∣ gcd c b)
id                                       └─┘  
src                                              
typ                                      └─┘  
148  (normalize_gcd  : ∀a b, normalize (gcd a b) = gcd a b)
id                         └───────┘  └─┘     └─┘  
src                          └───────┘           
typ                        └───────┘  └─┘     └─┘  
149  (gcd_mul_lcm    : ∀a b, gcd a b * lcm a b = normalize (a * b))
id                         └─┘    └─┘    └───────┘    
src                                            └───────┘    
typ                        └─┘    └─┘    └───────┘    
150  (lcm_zero_left  : ∀a, lcm 0 a = 0)
id                        └─┘    
src                                
typ                       └─┘    
151  (lcm_zero_right : ∀a, lcm a 0 = 0)
id                        └─┘    
src                                
typ                       └─┘    
152  end prio
153  
154  export gcd_domain (gcd lcm gcd_dvd_left gcd_dvd_right dvd_gcd  lcm_zero_left lcm_zero_right)
155  
156  attribute [simp] lcm_zero_left lcm_zero_right
id                    └───────────┘ └────────────┘
src                   └───────────┘ └────────────┘
typ                   └───────────┘ └────────────┘
doc             └──┘
157  
158  section gcd_domain
159  variables [gcd_domain α]
id              └────────┘
src             └────────┘
typ             └────────┘
doc             └────────┘
160  
161  @[simp] theorem normalize_gcd : ∀a b:α, normalize (gcd a b) = gcd a b :=
id                                          └───────┘  └─┘     └─┘  
src                                          └───────┘  └─┘       └─┘
typ                                         └───────┘  └─┘     └─┘  
doc    └──┘
162  gcd_domain.normalize_gcd
id   └──────────────────────┘
src  └──────────────────────┘
typ  └──────────────────────┘
163  
164  @[simp] theorem gcd_mul_lcm : ∀a b:α, gcd a b * lcm a b = normalize (a * b) :=
id                                        └─┘    └─┘    └───────┘    
src                                        └─┘      └─┘      └───────┘    
typ                                       └─┘    └─┘    └───────┘    
doc    └──┘
165  gcd_domain.gcd_mul_lcm
id   └────────────────────┘
src  └────────────────────┘
typ  └────────────────────┘
166  
167  section gcd
168  
169  theorem dvd_gcd_iff (a b c : α) : a ∣ gcd b c ↔ (a ∣ b ∧ a ∣ c) :=
id                                      └─┘           
src                                       └─┘               
typ                                     └─┘           
170  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
171    (assume h, ⟨dvd_trans h (gcd_dvd_left _ _), dvd_trans h (gcd_dvd_right _ _)⟩)
id                └───────┘   └──────────┘       └───────┘   └───────────┘
src                └───────┘    └──────────┘       └───────┘    └───────────┘
typ               └───────┘   └──────────┘       └───────┘   └───────────┘
172    (assume ⟨hab, hac⟩, dvd_gcd hab hac)
id             └─┘  └─┘   └─────┘
src                        └─────┘
typ            └─┘  └─┘   └─────┘
173  
174  theorem gcd_comm (a b : α) : gcd a b = gcd b a :=
id                               └─┘    └─┘  
src                               └─┘      └─┘
typ                              └─┘    └─┘  
175  dvd_antisymm_of_normalize_eq (normalize_gcd _ _) (normalize_gcd _ _)
id   └──────────────────────────┘  └───────────┘       └───────────┘
src  └──────────────────────────┘  └───────────┘       └───────────┘
typ  └──────────────────────────┘  └───────────┘       └───────────┘
176    (dvd_gcd (gcd_dvd_right _ _) (gcd_dvd_left _ _))
id      └─────┘  └───────────┘       └──────────┘
src     └─────┘  └───────────┘       └──────────┘
typ     └─────┘  └───────────┘       └──────────┘
177    (dvd_gcd (gcd_dvd_right _ _) (gcd_dvd_left _ _))
id      └─────┘  └───────────┘       └──────────┘
src     └─────┘  └───────────┘       └──────────┘
typ     └─────┘  └───────────┘       └──────────┘
178  
179  theorem gcd_assoc (m n k : α) : gcd (gcd m n) k = gcd m (gcd n k) :=
id                                  └─┘  └─┘      └─┘   └─┘  
src                                  └─┘  └─┘         └─┘    └─┘
typ                                 └─┘  └─┘      └─┘   └─┘  
180  dvd_antisymm_of_normalize_eq (normalize_gcd _ _) (normalize_gcd _ _)
id   └──────────────────────────┘  └───────────┘       └───────────┘
src  └──────────────────────────┘  └───────────┘       └───────────┘
typ  └──────────────────────────┘  └───────────┘       └───────────┘
181    (dvd_gcd
id      └─────┘
src     └─────┘
typ     └─────┘
182      (dvd.trans (gcd_dvd_left (gcd m n) k) (gcd_dvd_left m n))
id        └───────┘  └──────────┘  └─┘       └──────────┘  
src       └───────┘  └──────────┘  └─┘          └──────────┘
typ       └───────┘  └──────────┘  └─┘       └──────────┘  
183      (dvd_gcd (dvd.trans (gcd_dvd_left (gcd m n) k) (gcd_dvd_right m n)) (gcd_dvd_right (gcd m n) k)))
id        └─────┘  └───────┘  └──────────┘  └─┘       └───────────┘      └───────────┘  └─┘    
src       └─────┘  └───────┘  └──────────┘  └─┘          └───────────┘        └───────────┘  └─┘
typ       └─────┘  └───────┘  └──────────┘  └─┘       └───────────┘      └───────────┘  └─┘    
184    (dvd_gcd
id      └─────┘
src     └─────┘
typ     └─────┘
185      (dvd_gcd (gcd_dvd_left m (gcd n k)) (dvd.trans (gcd_dvd_right m (gcd n k)) (gcd_dvd_left n k)))
id        └─────┘  └──────────┘   └─┘      └───────┘  └───────────┘   └─┘      └──────────┘  
src       └─────┘  └──────────┘    └─┘        └───────┘  └───────────┘    └─┘        └──────────┘
typ       └─────┘  └──────────┘   └─┘      └───────┘  └───────────┘   └─┘      └──────────┘  
186      (dvd.trans (gcd_dvd_right m (gcd n k)) (gcd_dvd_right n k)))
id        └───────┘  └───────────┘   └─┘      └───────────┘  
src       └───────┘  └───────────┘    └─┘        └───────────┘
typ       └───────┘  └───────────┘   └─┘      └───────────┘  
187  
188  instance : is_commutative α gcd := ⟨gcd_comm⟩
id              └────────────┘  └─┘     └──────┘
src             └────────────┘   └─┘     └──────┘
typ             └────────────┘  └─┘     └──────┘
189  instance : is_associative α gcd := ⟨gcd_assoc⟩
id              └────────────┘  └─┘     └───────┘
src             └────────────┘   └─┘     └───────┘
typ             └────────────┘  └─┘     └───────┘
190  
191  theorem gcd_eq_normalize {a b c : α} (habc : gcd a b ∣ c) (hcab : c ∣ gcd a b) :
id                                               └─┘                └─┘  
src                                               └─┘                    └─┘
typ                                              └─┘                └─┘  
192    gcd a b = normalize c :=
id     └─┘    └───────┘ 
src    └─┘      └───────┘
typ    └─┘    └───────┘ 
193  normalize_gcd a b ▸ normalize_eq_normalize habc hcab
id   └───────────┘    └────────────────────┘ └──┘ └──┘
src  └───────────┘      └────────────────────┘
typ  └───────────┘    └────────────────────┘ └──┘ └──┘
194  
195  @[simp] theorem gcd_zero_left (a : α) : gcd 0 a = normalize a :=
id                                          └─┘     └───────┘ 
src                                          └─┘      └───────┘
typ                                         └─┘     └───────┘ 
doc    └──┘
196  gcd_eq_normalize (gcd_dvd_right 0 a) (dvd_gcd (dvd_zero _) (dvd_refl a))
id   └──────────────┘  └───────────┘      └─────┘  └──────┘     └──────┘ 
src  └──────────────┘  └───────────┘       └─────┘  └──────┘     └──────┘
typ  └──────────────┘  └───────────┘      └─────┘  └──────┘     └──────┘ 
197  
198  @[simp] theorem gcd_zero_right (a : α) : gcd a 0 = normalize a :=
id                                           └─┘     └───────┘ 
src                                           └─┘      └───────┘
typ                                          └─┘     └───────┘ 
doc    └──┘
199  gcd_eq_normalize (gcd_dvd_left a 0) (dvd_gcd (dvd_refl a) (dvd_zero _))
id   └──────────────┘  └──────────┘      └─────┘  └──────┘    └──────┘
src  └──────────────┘  └──────────┘       └─────┘  └──────┘     └──────┘
typ  └──────────────┘  └──────────┘      └─────┘  └──────┘    └──────┘
200  
201  @[simp] theorem gcd_eq_zero_iff (a b : α) : gcd a b = 0 ↔ a = 0 ∧ b = 0 :=
id                                              └─┘             
src                                              └─┘                 
typ                                             └─┘             
doc    └──┘
202  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
203    (assume h, let ⟨ca, ha⟩ := gcd_dvd_left a b, ⟨cb, hb⟩ := gcd_dvd_right a b in
id               └─┘             └──────────┘                └───────────┘  
src                               └──────────┘                  └───────────┘
typ              └─┘             └──────────┘                └───────────┘  
204      by rw [h, zero_mul] at ha hb; exact ⟨ha, hb⟩)
id                └──────┘                   └┘  └┘
src         └──┘ └┘└──────┘└────────┘  └────┘   └┘  
typ         └──┘└┘└──────┘└────────┘  └────┘ └┘└┘└┘
doc         └──┘ └┘        └────────┘  └────┘   └┘  
txt         └──┘ └┘        └────────┘  └────┘   └┘  
par         └──┘ └┘        └────────┘  └────┘   └┘  
pid           └┘ └┘        └───────┘          └┘  
st         └────┘└────────┘└───────────────────────┘
205    (assume ⟨ha, hb⟩, by rw [ha, hb, gcd_zero_left, normalize_zero])
id                             └┘  └┘  └───────────┘  └────────────┘
src                         └──┘  └┘  └┘└───────────┘└┘└────────────┘
typ                        └──┘└┘└┘└┘└┘└───────────┘└┘└────────────┘
doc                         └──┘  └┘  └┘             └┘              
txt                         └──┘  └┘  └┘             └┘              
par                         └──┘  └┘  └┘             └┘              
pid                           └┘  └┘  └┘             └┘              
st                         └─────┘└──┘└─────────────┘└──────────────┘
206  
207  @[simp] theorem gcd_one_left (a : α) : gcd 1 a = 1 :=
id                                         └─┘    
src                                         └─┘     
typ                                        └─┘    
doc    └──┘
208  dvd_antisymm_of_normalize_eq (normalize_gcd _ _) normalize_one (gcd_dvd_left _ _) (one_dvd _)
id   └──────────────────────────┘  └───────────┘      └───────────┘  └──────────┘       └─────┘
src  └──────────────────────────┘  └───────────┘      └───────────┘  └──────────┘       └─────┘
typ  └──────────────────────────┘  └───────────┘      └───────────┘  └──────────┘       └─────┘
209  
210  @[simp] theorem gcd_one_right (a : α) : gcd a 1 = 1 :=
id                                          └─┘    
src                                          └─┘     
typ                                         └─┘    
doc    └──┘
211  dvd_antisymm_of_normalize_eq (normalize_gcd _ _) normalize_one (gcd_dvd_right _ _) (one_dvd _)
id   └──────────────────────────┘  └───────────┘      └───────────┘  └───────────┘       └─────┘
src  └──────────────────────────┘  └───────────┘      └───────────┘  └───────────┘       └─────┘
typ  └──────────────────────────┘  └───────────┘      └───────────┘  └───────────┘       └─────┘
212  
213  theorem gcd_dvd_gcd {a b c d: α} (hab : a ∣ b) (hcd : c ∣ d) : gcd a c ∣ gcd b d :=
id                                                           └─┘    └─┘  
src                                                               └─┘      └─┘
typ                                                          └─┘    └─┘  
214  dvd_gcd (dvd.trans (gcd_dvd_left _ _) hab) (dvd.trans (gcd_dvd_right _ _) hcd)
id   └─────┘  └───────┘  └──────────┘      └─┘   └───────┘  └───────────┘      └─┘
src  └─────┘  └───────┘  └──────────┘            └───────┘  └───────────┘
typ  └─────┘  └───────┘  └──────────┘      └─┘   └───────┘  └───────────┘      └─┘
215  
216  @[simp] theorem gcd_same (a : α) : gcd a a = normalize a :=
id                                     └─┘    └───────┘ 
src                                     └─┘      └───────┘
typ                                    └─┘    └───────┘ 
doc    └──┘
217  gcd_eq_normalize (gcd_dvd_left _ _) (dvd_gcd (dvd_refl a) (dvd_refl a))
id   └──────────────┘  └──────────┘       └─────┘  └──────┘    └──────┘ 
src  └──────────────┘  └──────────┘       └─────┘  └──────┘     └──────┘
typ  └──────────────┘  └──────────┘       └─────┘  └──────┘    └──────┘ 
218  
219  @[simp] theorem gcd_mul_left (a b c : α) : gcd (a * b) (a * c) = normalize a * gcd b c :=
id                                             └─┘            └───────┘   └─┘  
src                                             └─┘                └───────┘    └─┘
typ                                            └─┘            └───────┘   └─┘  
doc    └──┘
220  classical.by_cases (by rintro rfl; simp only [zero_mul, gcd_zero_left, normalize_zero]) $ assume ha : a ≠ 0,
id   └────────────────┘                            └──────┘  └───────────┘  └────────────┘                  
src  └────────────────┘     └────────┘  └─────────┘└──────┘└┘└───────────┘└┘└────────────┘                  
typ  └────────────────┘     └────────┘  └─────────┘└──────┘└┘└───────────┘└┘└────────────┘                 
doc                         └────────┘  └─────────┘        └┘             └┘              
txt                         └────────┘  └─────────┘        └┘             └┘              
par                         └────────┘  └─────────┘        └┘             └┘              
pid                               └──┘      └──┘└┘        └┘             └┘              
st                         └──────────────────────────────────────────────────────────────┘
221  suffices gcd (a * b) (a * c) = normalize (a * gcd b c),
id            └─┘            └───────┘    └─┘  
src           └─┘                └───────┘     └─┘
typ           └─┘            └───────┘    └─┘  
222    by simpa only [normalize_mul, normalize_gcd],
id                    └───────────┘  └───────────┘
src       └──────────┘└───────────┘└┘└───────────┘
typ       └──────────┘└───────────┘└┘└───────────┘
doc       └──────────┘             └┘             
txt       └──────────┘             └┘             
par       └──────────┘             └┘             
pid            └──┘└┘             └┘             
st       └────────────────────────────────────────┘
223  let ⟨d, eq⟩ := dvd_gcd (dvd_mul_right a b) (dvd_mul_right a c) in
id   └─┘    └┘     └─────┘  └───────────┘     └───────────┘  
src          └┘     └─────┘  └───────────┘       └───────────┘
typ  └─┘    └┘     └─────┘  └───────────┘     └───────────┘  
224  gcd_eq_normalize
id   └──────────────┘
src  └──────────────┘
typ  └──────────────┘
225    (eq.symm ▸ mul_dvd_mul_left a $ show d ∣ gcd b c, from
id        └───┘  └──────────────┘            └─┘  
src       └───┘  └──────────────┘             └─┘
typ       └───┘  └──────────────┘            └─┘  
226      dvd_gcd
id       └─────┘
src      └─────┘
typ      └─────┘
227        ((mul_dvd_mul_iff_left ha).1 $ eq ▸ gcd_dvd_left _ _)
id           └──────────────────┘ └┘         └──────────┘
src          └──────────────────┘            └──────────┘
typ          └──────────────────┘ └┘         └──────────┘
doc          └──────────────────┘
228        ((mul_dvd_mul_iff_left ha).1 $ eq ▸ gcd_dvd_right _ _))
id           └──────────────────┘ └┘         └───────────┘
src          └──────────────────┘            └───────────┘
typ          └──────────────────┘ └┘         └───────────┘
doc          └──────────────────┘
229    (dvd_gcd
id      └─────┘
src     └─────┘
typ     └─────┘
230      (mul_dvd_mul_left a $ gcd_dvd_left _ _)
id        └──────────────┘    └──────────┘
src       └──────────────┘     └──────────┘
typ       └──────────────┘    └──────────┘
231      (mul_dvd_mul_left a $ gcd_dvd_right _ _))
id        └──────────────┘    └───────────┘
src       └──────────────┘     └───────────┘
typ       └──────────────┘    └───────────┘
232  
233  @[simp] theorem gcd_mul_right (a b c : α) : gcd (b * a) (c * a) = gcd b c * normalize a :=
id                                              └─┘            └─┘    └───────┘ 
src                                              └─┘                └─┘      └───────┘
typ                                             └─┘            └─┘    └───────┘ 
doc    └──┘
234  by simp only [mul_comm, gcd_mul_left]
id                 └──────┘  └──────────┘
src     └─────────┘└──────┘└┘└──────────┘└─
typ     └─────────┘└──────┘└┘└──────────┘└─
doc     └─────────┘        └┘            └─
txt     └─────────┘        └┘            └─
par     └─────────┘        └┘            └─
pid         └──┘└┘        └┘            
st     └───────────────────────────────────
235  
src  
typ  
doc  
txt  
par  
pid  
st   
236  theorem gcd_eq_left_iff (a b : α) (h : normalize a = a) : gcd a b = a ↔ a ∣ b :=
id                                         └───────┘       └─┘        
src                                         └───────┘         └─┘           
typ                                        └───────┘       └─┘        
237  iff.intro (assume eq, eq ▸ gcd_dvd_right _ _) $
id   └───────┘         └┘  └┘  └───────────┘
src  └───────┘         └┘  └┘  └───────────┘
typ  └───────┘         └┘  └┘  └───────────┘
238    assume hab, dvd_antisymm_of_normalize_eq (normalize_gcd _ _) h (gcd_dvd_left _ _) (dvd_gcd (dvd_refl a) hab)
id            └─┘  └──────────────────────────┘  └───────────┘        └──────────┘       └─────┘  └──────┘   └─┘
src                └──────────────────────────┘  └───────────┘         └──────────┘       └─────┘  └──────┘
typ           └─┘  └──────────────────────────┘  └───────────┘        └──────────┘       └─────┘  └──────┘   └─┘
239  
240  theorem gcd_eq_right_iff (a b : α) (h : normalize b = b) : gcd a b = b ↔ b ∣ a :=
id                                          └───────┘       └─┘        
src                                          └───────┘         └─┘           
typ                                         └───────┘       └─┘        
241  by simpa only [gcd_comm a b] using gcd_eq_left_iff b a h
id                  └──────┘          └─────────────┘   
src     └──────────┘└──────┘  └──────┘└─────────────┘   
typ     └──────────┘└──────┘└──────┘└─────────────┘
doc     └──────────┘          └──────┘                  
txt     └──────────┘          └──────┘                  
par     └──────────┘          └──────┘                  
pid          └──┘└┘          └────┘                  
st     └──────────────────────────────────────────────────────
242  
src  
typ  
doc  
txt  
par  
pid  
st   
243  theorem gcd_dvd_gcd_mul_left (m n k : α) : gcd m n ∣ gcd (k * m) n :=
id                                             └─┘    └─┘      
src                                             └─┘      └─┘    
typ                                            └─┘    └─┘      
244  gcd_dvd_gcd (dvd_mul_left _ _) (dvd_refl _)
id   └─────────┘  └──────────┘       └──────┘
src  └─────────┘  └──────────┘       └──────┘
typ  └─────────┘  └──────────┘       └──────┘
245  
246  theorem gcd_dvd_gcd_mul_right (m n k : α) : gcd m n ∣ gcd (m * k) n :=
id                                              └─┘    └─┘      
src                                              └─┘      └─┘    
typ                                             └─┘    └─┘      
247  gcd_dvd_gcd (dvd_mul_right _ _) (dvd_refl _)
id   └─────────┘  └───────────┘       └──────┘
src  └─────────┘  └───────────┘       └──────┘
typ  └─────────┘  └───────────┘       └──────┘
248  
249  theorem gcd_dvd_gcd_mul_left_right (m n k : α) : gcd m n ∣ gcd m (k * n) :=
id                                                   └─┘    └─┘     
src                                                   └─┘      └─┘      
typ                                                  └─┘    └─┘     
250  gcd_dvd_gcd (dvd_refl _) (dvd_mul_left _ _)
id   └─────────┘  └──────┘     └──────────┘
src  └─────────┘  └──────┘     └──────────┘
typ  └─────────┘  └──────┘     └──────────┘
251  
252  theorem gcd_dvd_gcd_mul_right_right (m n k : α) : gcd m n ∣ gcd m (n * k) :=
id                                                    └─┘    └─┘     
src                                                    └─┘      └─┘      
typ                                                   └─┘    └─┘     
253  gcd_dvd_gcd (dvd_refl _) (dvd_mul_right _ _)
id   └─────────┘  └──────┘     └───────────┘
src  └─────────┘  └──────┘     └───────────┘
typ  └─────────┘  └──────┘     └───────────┘
254  
255  end gcd
256  
257  section lcm
258  
259  lemma lcm_dvd_iff {a b c : α} : lcm a b ∣ c ↔ a ∣ c ∧ b ∣ c :=
id                                  └─┘            
src                                  └─┘                 
typ                                 └─┘            
260  classical.by_cases
id   └────────────────┘
src  └────────────────┘
typ  └────────────────┘
261    (assume : a = 0 ∨ b = 0, by rcases this with rfl | rfl;
id                                   └──┘
src                             └─────┘    └─────────────┘
typ                           └─────┘└──┘└─────────────┘
doc                                └─────┘    └─────────────┘
txt                                └─────┘    └─────────────┘
par                                └─────┘    └─────────────┘
pid                                          └─────────────┘
st                                └────────────────────────────
262      simp only [iff_def, lcm_zero_left, lcm_zero_right, zero_dvd_iff, dvd_zero,
id                  └─────┘  └───────────┘  └────────────┘  └──────────┘  └──────┘
src      └─────────┘└─────┘└┘└───────────┘└┘└────────────┘└┘└──────────┘└┘└──────┘└─
typ      └─────────┘└─────┘└┘└───────────┘└┘└────────────┘└┘└──────────┘└┘└──────┘└─
doc      └─────────┘       └┘             └┘              └┘└──────────┘└┘        └─
txt      └─────────┘       └┘             └┘              └┘            └┘        └─
par      └─────────┘       └┘             └┘              └┘            └┘        └─
pid          └──┘└┘       └┘             └┘              └┘            └┘        └─
st   ───────────────────────────────────────────────────────────────────────────────
263        eq_self_iff_true, and_true, imp_true_iff] {contextual:=tt})
id         └──────────────┘  └──────┘  └──────────┘               └┘
src  ─────┘└──────────────┘└┘└──────┘└┘└──────────┘└┘ └──────────┘└┘
typ  ─────┘└──────────────┘└┘└──────┘└┘└──────────┘└┘ └──────────┘└┘
doc  ─────┘                └┘        └┘            └┘ └──────────┘  
txt  ─────┘                └┘        └┘            └┘ └──────────┘  
par  ─────┘                └┘        └┘            └┘ └──────────┘  
pid  ─────┘                └┘        └┘             └──────────┘  
st   ───────────────────────────────────────────────────────────────┘
264    (assume this : ¬ (a = 0 ∨ b = 0),
id                            
src                             
typ                           
265      let ⟨h1, h2⟩ := not_or_distrib.1 this in
id       └─┘  └┘         └────────────┘  └──┘
src                      └────────────┘
typ      └─┘  └┘         └────────────┘  └──┘
266      have h : gcd a b ≠ 0, from λ H, h1 ((gcd_eq_zero_iff _ _).1 H).1,
id                └─┘                     └─────────────┘        
src               └─┘                        └─────────────┘         
typ               └─┘                     └─────────────┘        
267      by rw [← mul_dvd_mul_iff_left h, gcd_mul_lcm, normalize_dvd_iff, ← dvd_normalize_iff,
id                └──────────────────┘   └─────────┘  └───────────────┘    └───────────────┘
src         └────┘└──────────────────┘ └┘└─────────┘└┘└───────────────┘└──┘└───────────────┘└─
typ         └────┘└──────────────────┘└┘└─────────┘└┘└───────────────┘└──┘└───────────────┘└─
doc         └────┘└──────────────────┘ └┘           └┘                 └──┘                 └─
txt         └────┘                     └┘           └┘                 └──┘                 └─
par         └────┘                     └┘           └┘                 └──┘                 └─
pid           └──┘                     └┘           └┘                 └──┘                 └─
st         └───────────────────────────┘└───────────┘└─────────────────┘└───────────────────┘└─
268          normalize_mul, normalize_gcd, ← gcd_mul_right, dvd_gcd_iff,
id           └───────────┘  └───────────┘    └───────────┘  └─────────┘
src  ───────┘└───────────┘└┘└───────────┘└──┘└───────────┘└┘└─────────┘└─
typ  ───────┘└───────────┘└┘└───────────┘└──┘└───────────┘└┘└─────────┘└─
doc  ───────┘             └┘             └──┘             └┘           └─
txt  ───────┘             └┘             └──┘             └┘           └─
par  ───────┘             └┘             └──┘             └┘           └─
pid  ───────┘             └┘             └──┘             └┘           └─
st   ────────────────────┘└─────────────┘└───────────────┘└───────────┘└─
269          mul_comm b c, mul_dvd_mul_iff_left h1, mul_dvd_mul_iff_right h2, and_comm])
id           └──────┘    └──────────────────┘ └┘  └───────────────────┘ └┘  └──────┘
src  ───────┘└──────┘  └┘└──────────────────┘  └┘└───────────────────┘  └┘└──────┘
typ  ───────┘└──────┘└┘└──────────────────┘└┘└┘└───────────────────┘└┘└┘└──────┘
doc  ───────┘          └┘└──────────────────┘  └┘└───────────────────┘  └┘        
txt  ───────┘          └┘                      └┘                       └┘        
par  ───────┘          └┘                      └┘                       └┘        
pid  ───────┘          └┘                      └┘                       └┘        
st   ───────────────────┘└───────────────────────┘└────────────────────────┘└────────┘
270  
271  lemma dvd_lcm_left (a b : α) : a ∣ lcm a b := (lcm_dvd_iff.1 (dvd_refl _)).1
id                                   └─┘       └─────────┘   └──────┘    
src                                    └─┘         └─────────┘   └──────┘    
typ                                  └─┘       └─────────┘   └──────┘    
272  
273  lemma dvd_lcm_right (a b : α) : b ∣ lcm a b := (lcm_dvd_iff.1 (dvd_refl _)).2
id                                    └─┘       └─────────┘   └──────┘    
src                                     └─┘         └─────────┘   └──────┘    
typ                                   └─┘       └─────────┘   └──────┘    
274  
275  lemma lcm_dvd {a b c : α} (hab : a ∣ b) (hcb : c ∣ b) : lcm a c ∣ b :=
id                                                    └─┘    
src                                                        └─┘     
typ                                                   └─┘    
276  lcm_dvd_iff.2 ⟨hab, hcb⟩
id   └─────────┘   └─┘  └─┘
src  └─────────┘
typ  └─────────┘   └─┘  └─┘
277  
278  @[simp] theorem lcm_eq_zero_iff (a b : α) : lcm a b = 0 ↔ a = 0 ∨ b = 0 :=
id                                              └─┘             
src                                              └─┘                 
typ                                             └─┘             
doc    └──┘
279  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
280    (assume h : lcm a b = 0,
id                 └─┘   
src                └─┘     
typ                └─┘   
281      have normalize (a * b) = 0,
id            └───────┘      
src           └───────┘        
typ           └───────┘      
282        by rw [← gcd_mul_lcm _ _, h, mul_zero],
id                  └─────────┘        └──────┘
src           └────┘└─────────┘└────┘ └┘└──────┘
typ           └────┘└─────────┘└────┘└┘└──────┘
doc           └────┘           └────┘ └┘        
txt           └────┘           └────┘ └┘        
par           └────┘           └────┘ └┘        
pid             └──┘           └────┘ └┘        
st           └────────────────────┘└─┘└────────┘
283      by simpa only [normalize_eq_zero, mul_eq_zero, units.ne_zero, or_false])
id                      └───────────────┘  └─────────┘  └───────────┘  └──────┘
src         └──────────┘└───────────────┘└┘└─────────┘└┘└───────────┘└┘└──────┘
typ         └──────────┘└───────────────┘└┘└─────────┘└┘└───────────┘└┘└──────┘
doc         └──────────┘                 └┘└─────────┘└┘└───────────┘└┘        
txt         └──────────┘                 └┘           └┘             └┘        
par         └──────────┘                 └┘           └┘             └┘        
pid              └──┘└┘                 └┘           └┘             └┘        
st         └───────────────────────────────────────────────────────────────────┘
284    (by rintro (rfl | rfl); [apply lcm_zero_left, apply lcm_zero_right])
id                                   └───────────┘        └────────────┘
src        └────────────────┘  └────┘└───────────┘  └────┘└────────────┘
typ        └────────────────┘  └────┘└───────────┘  └────┘└────────────┘
doc        └────────────────┘   └────┘               └────┘
txt        └────────────────┘   └────┘               └────┘
par        └────────────────┘   └────┘               └────┘
pid              └──────────┘                            
st        └──────────────────────────────────────────────────────────────┘
285  
286  @[simp] lemma normalize_lcm (a b : α) : normalize (lcm a b) = lcm a b :=
id                                          └───────┘  └─┘     └─┘  
src                                          └───────┘  └─┘       └─┘
typ                                         └───────┘  └─┘     └─┘  
doc    └──┘
287  classical.by_cases (assume : lcm a b = 0, by rw [this, normalize_zero]) $
id   └────────────────┘           └─┘              └──┘  └────────────┘
src  └────────────────┘           └─┘            └──┘    └┘└────────────┘
typ  └────────────────┘           └─┘          └──┘└──┘└┘└────────────┘
doc                                               └──┘    └┘              
txt                                               └──┘    └┘              
par                                               └──┘    └┘              
pid                                                 └┘    └┘              
st                                               └───────┘└──────────────┘
288    assume h_lcm : lcm a b ≠ 0,
id                    └─┘   
src                   └─┘     
typ                   └─┘   
289    have h1 : gcd a b ≠ 0, from mt (by rw [gcd_eq_zero_iff, lcm_eq_zero_iff];
id               └─┘            └┘         └─────────────┘  └─────────────┘
src              └─┘              └┘     └──┘└─────────────┘└┘└─────────────┘
typ              └─┘            └┘     └──┘└─────────────┘└┘└─────────────┘
doc                                       └──┘               └┘               
txt                                       └──┘               └┘               
par                                       └──┘               └┘               
pid                                         └┘               └┘               
st                                       └──────────────────┘└───────────────┘└─
290      rintros ⟨rfl, rfl⟩; left; refl) h_lcm,
id                                       └───┘
src      └────────────────┘  └──┘  └──┘
typ      └────────────────┘  └──┘  └──┘  └───┘
doc      └────────────────┘  └──┘  └──┘
txt      └────────────────┘  └──┘  └──┘
par      └────────────────┘  └──┘  └──┘
pid             └─────────┘
st   ─────────────────────────────────┘
291    have h2 : normalize (gcd a b * lcm a b) = gcd a b * lcm a b,
id               └───────┘  └─┘    └─┘     └─┘    └─┘  
src              └───────┘  └─┘      └─┘       └─┘      └─┘
typ              └───────┘  └─┘    └─┘     └─┘    └─┘  
292      by rw [gcd_mul_lcm, normalize_idem],
id              └─────────┘  └────────────┘
src         └──┘└─────────┘└┘└────────────┘
typ         └──┘└─────────┘└┘└────────────┘
doc         └──┘           └┘              
txt         └──┘           └┘              
par         └──┘           └┘              
pid           └┘           └┘              
st         └──────────────┘└──────────────┘
293    by simpa only [normalize_mul, normalize_gcd, one_mul, domain.mul_left_inj h1] using h2
id                    └───────────┘  └───────────┘  └─────┘  └─────────────────┘ └┘        └┘
src       └──────────┘└───────────┘└┘└───────────┘└┘└─────┘└┘└─────────────────┘  └──────┘  
typ       └──────────┘└───────────┘└┘└───────────┘└┘└─────┘└┘└─────────────────┘└┘└──────┘└┘
doc       └──────────┘             └┘             └┘       └┘└─────────────────┘  └──────┘  
txt       └──────────┘             └┘             └┘       └┘                     └──────┘  
par       └──────────┘             └┘             └┘       └┘                     └──────┘  
pid            └──┘└┘             └┘             └┘       └┘                     └────┘  
st       └────────────────────────────────────────────────────────────────────────────────────
294  
src  
typ  
doc  
txt  
par  
pid  
st   
295  theorem lcm_comm (a b : α) : lcm a b = lcm b a :=
id                               └─┘    └─┘  
src                               └─┘      └─┘
typ                              └─┘    └─┘  
296  dvd_antisymm_of_normalize_eq (normalize_lcm _ _) (normalize_lcm _ _)
id   └──────────────────────────┘  └───────────┘       └───────────┘
src  └──────────────────────────┘  └───────────┘       └───────────┘
typ  └──────────────────────────┘  └───────────┘       └───────────┘
297    (lcm_dvd (dvd_lcm_right _ _) (dvd_lcm_left _ _))
id      └─────┘  └───────────┘       └──────────┘
src     └─────┘  └───────────┘       └──────────┘
typ     └─────┘  └───────────┘       └──────────┘
298    (lcm_dvd (dvd_lcm_right _ _) (dvd_lcm_left _ _))
id      └─────┘  └───────────┘       └──────────┘
src     └─────┘  └───────────┘       └──────────┘
typ     └─────┘  └───────────┘       └──────────┘
299  
300  theorem lcm_assoc (m n k : α) : lcm (lcm m n) k = lcm m (lcm n k) :=
id                                  └─┘  └─┘      └─┘   └─┘  
src                                  └─┘  └─┘         └─┘    └─┘
typ                                 └─┘  └─┘      └─┘   └─┘  
301  dvd_antisymm_of_normalize_eq (normalize_lcm _ _) (normalize_lcm _ _)
id   └──────────────────────────┘  └───────────┘       └───────────┘
src  └──────────────────────────┘  └───────────┘       └───────────┘
typ  └──────────────────────────┘  └───────────┘       └───────────┘
302    (lcm_dvd
id      └─────┘
src     └─────┘
typ     └─────┘
303      (lcm_dvd (dvd_lcm_left _ _) (dvd.trans (dvd_lcm_left _ _) (dvd_lcm_right _ _)))
id        └─────┘  └──────────┘       └───────┘  └──────────┘       └───────────┘
src       └─────┘  └──────────┘       └───────┘  └──────────┘       └───────────┘
typ       └─────┘  └──────────┘       └───────┘  └──────────┘       └───────────┘
304      (dvd.trans (dvd_lcm_right _ _) (dvd_lcm_right _ _)))
id        └───────┘  └───────────┘       └───────────┘
src       └───────┘  └───────────┘       └───────────┘
typ       └───────┘  └───────────┘       └───────────┘
305    (lcm_dvd
id      └─────┘
src     └─────┘
typ     └─────┘
306      (dvd.trans (dvd_lcm_left _ _) (dvd_lcm_left _ _))
id        └───────┘  └──────────┘       └──────────┘
src       └───────┘  └──────────┘       └──────────┘
typ       └───────┘  └──────────┘       └──────────┘
307      (lcm_dvd (dvd.trans (dvd_lcm_right _ _) (dvd_lcm_left _ _)) (dvd_lcm_right _ _)))
id        └─────┘  └───────┘  └───────────┘       └──────────┘        └───────────┘
src       └─────┘  └───────┘  └───────────┘       └──────────┘        └───────────┘
typ       └─────┘  └───────┘  └───────────┘       └──────────┘        └───────────┘
308  
309  instance : is_commutative α lcm := ⟨lcm_comm⟩
id              └────────────┘  └─┘     └──────┘
src             └────────────┘   └─┘     └──────┘
typ             └────────────┘  └─┘     └──────┘
310  instance : is_associative α lcm := ⟨lcm_assoc⟩
id              └────────────┘  └─┘     └───────┘
src             └────────────┘   └─┘     └───────┘
typ             └────────────┘  └─┘     └───────┘
311  
312  lemma lcm_eq_normalize {a b c : α} (habc : lcm a b ∣ c) (hcab : c ∣ lcm a b) :
id                                             └─┘                └─┘  
src                                             └─┘                    └─┘
typ                                            └─┘                └─┘  
313    lcm a b = normalize c :=
id     └─┘    └───────┘ 
src    └─┘      └───────┘
typ    └─┘    └───────┘ 
314  normalize_lcm a b ▸ normalize_eq_normalize habc hcab
id   └───────────┘    └────────────────────┘ └──┘ └──┘
src  └───────────┘      └────────────────────┘
typ  └───────────┘    └────────────────────┘ └──┘ └──┘
315  
316  theorem lcm_dvd_lcm {a b c d : α} (hab : a ∣ b) (hcd : c ∣ d) : lcm a c ∣ lcm b d :=
id                                                            └─┘    └─┘  
src                                                                └─┘      └─┘
typ                                                           └─┘    └─┘  
317  lcm_dvd (dvd.trans hab (dvd_lcm_left _ _)) (dvd.trans hcd (dvd_lcm_right _ _))
id   └─────┘  └───────┘ └─┘  └──────────┘        └───────┘ └─┘  └───────────┘
src  └─────┘  └───────┘      └──────────┘        └───────┘      └───────────┘
typ  └─────┘  └───────┘ └─┘  └──────────┘        └───────┘ └─┘  └───────────┘
318  
319  @[simp] theorem lcm_units_coe_left (u : units α) (a : α) : lcm ↑u a = normalize a :=
id                                           └───┘            └─┘    └───────┘ 
src                                          └───┘              └─┘      └───────┘
typ                                          └───┘            └─┘    └───────┘ 
doc    └──┘
320  lcm_eq_normalize (lcm_dvd (units.coe_dvd _ _) (dvd_refl _)) (dvd_lcm_right _ _)
id   └──────────────┘  └─────┘  └───────────┘       └──────┘      └───────────┘
src  └──────────────┘  └─────┘  └───────────┘       └──────┘      └───────────┘
typ  └──────────────┘  └─────┘  └───────────┘       └──────┘      └───────────┘
doc                             └───────────┘
321  
322  @[simp] theorem lcm_units_coe_right (a : α) (u : units α) : lcm a ↑u = normalize a :=
id                                                   └───┘     └─┘    └───────┘ 
src                                                   └───┘      └─┘      └───────┘
typ                                                  └───┘     └─┘    └───────┘ 
doc    └──┘
323  (lcm_comm a u).trans $ lcm_units_coe_left _ _
id    └──────┘   └───┘    └────────────────┘
src   └──────┘     └───┘    └────────────────┘
typ   └──────┘   └───┘    └────────────────┘
324  
325  @[simp] theorem lcm_one_left (a : α) : lcm 1 a = normalize a :=
id                                         └─┘     └───────┘ 
src                                         └─┘      └───────┘
typ                                        └─┘     └───────┘ 
doc    └──┘
326  lcm_units_coe_left 1 a
id   └────────────────┘   
src  └────────────────┘
typ  └────────────────┘   
327  
328  @[simp] theorem lcm_one_right (a : α) : lcm a 1 = normalize a :=
id                                          └─┘     └───────┘ 
src                                          └─┘      └───────┘
typ                                         └─┘     └───────┘ 
doc    └──┘
329  lcm_units_coe_right a 1
id   └─────────────────┘ 
src  └─────────────────┘
typ  └─────────────────┘ 
330  
331  @[simp] theorem lcm_same (a : α) : lcm a a = normalize a :=
id                                     └─┘    └───────┘ 
src                                     └─┘      └───────┘
typ                                    └─┘    └───────┘ 
doc    └──┘
332  lcm_eq_normalize (lcm_dvd (dvd_refl _) (dvd_refl _)) (dvd_lcm_left _ _)
id   └──────────────┘  └─────┘  └──────┘     └──────┘      └──────────┘
src  └──────────────┘  └─────┘  └──────┘     └──────┘      └──────────┘
typ  └──────────────┘  └─────┘  └──────┘     └──────┘      └──────────┘
333  
334  @[simp] theorem lcm_eq_one_iff (a b : α) : lcm a b = 1 ↔ a ∣ 1 ∧ b ∣ 1 :=
id                                             └─┘             
src                                             └─┘                 
typ                                            └─┘             
doc    └──┘
335  iff.intro
id   └───────┘
src  └───────┘
typ  └───────┘
336    (assume eq, eq ▸ ⟨dvd_lcm_left _ _, dvd_lcm_right _ _⟩)
id             └┘  └┘   └──────────┘      └───────────┘
src            └┘  └┘   └──────────┘      └───────────┘
typ            └┘  └┘   └──────────┘      └───────────┘
337    (assume ⟨⟨c, hc⟩, ⟨d, hd⟩⟩,
id                └┘      └┘
typ               └┘      └┘
338      show lcm (units.mk_of_mul_eq_one a c hc.symm : α) (units.mk_of_mul_eq_one b d hd.symm) = 1,
id            └─┘  └────────────────────┘      └───┘      └────────────────────┘      └───┘  
src           └─┘  └────────────────────┘       └───┘       └────────────────────┘       └───┘  
typ           └─┘  └────────────────────┘      └───┘      └────────────────────┘      └───┘  
339        by rw [lcm_units_coe_left, normalize_coe_units])
id                └────────────────┘  └─────────────────┘
src           └──┘└────────────────┘└┘└─────────────────┘
typ           └──┘└────────────────┘└┘└─────────────────┘
doc           └──┘                  └┘                   
txt           └──┘                  └┘                   
par           └──┘                  └┘                   
pid             └┘                  └┘                   
st           └─────────────────────┘└───────────────────┘
340  
341  @[simp] theorem lcm_mul_left (a b c : α) : lcm (a * b) (a * c) = normalize a * lcm b c :=
id                                             └─┘            └───────┘   └─┘  
src                                             └─┘                └───────┘    └─┘
typ                                            └─┘            └───────┘   └─┘  
doc    └──┘
342  classical.by_cases (by rintro rfl; simp only [zero_mul, lcm_zero_left, normalize_zero]) $ assume ha : a ≠ 0,
id   └────────────────┘                            └──────┘  └───────────┘  └────────────┘                  
src  └────────────────┘     └────────┘  └─────────┘└──────┘└┘└───────────┘└┘└────────────┘                  
typ  └────────────────┘     └────────┘  └─────────┘└──────┘└┘└───────────┘└┘└────────────┘                 
doc                         └────────┘  └─────────┘        └┘             └┘              
txt                         └────────┘  └─────────┘        └┘             └┘              
par                         └────────┘  └─────────┘        └┘             └┘              
pid                               └──┘      └──┘└┘        └┘             └┘              
st                         └──────────────────────────────────────────────────────────────┘
343  suffices lcm (a * b) (a * c) = normalize (a * lcm b c),
id            └─┘            └───────┘    └─┘  
src           └─┘                └───────┘     └─┘
typ           └─┘            └───────┘    └─┘  
344    by simpa only [normalize_mul, normalize_lcm],
id                    └───────────┘  └───────────┘
src       └──────────┘└───────────┘└┘└───────────┘
typ       └──────────┘└───────────┘└┘└───────────┘
doc       └──────────┘             └┘             
txt       └──────────┘             └┘             
par       └──────────┘             └┘             
pid            └──┘└┘             └┘             
st       └────────────────────────────────────────┘
345  have a ∣ lcm (a * b) (a * c), from dvd.trans (dvd_mul_right _ _) (dvd_lcm_left _ _),
id          └─┘                 └───────┘  └───────────┘       └──────────┘
src          └─┘                     └───────┘  └───────────┘       └──────────┘
typ         └─┘                 └───────┘  └───────────┘       └──────────┘
346  let ⟨d, eq⟩ := this in
id   └─┘     └┘     └──┘
src          └┘
typ  └─┘     └┘     └──┘
347  lcm_eq_normalize
id   └──────────────┘
src  └──────────────┘
typ  └──────────────┘
348    (lcm_dvd (mul_dvd_mul_left a (dvd_lcm_left _ _)) (mul_dvd_mul_left a (dvd_lcm_right _ _)))
id      └─────┘  └──────────────┘   └──────────┘        └──────────────┘   └───────────┘
src     └─────┘  └──────────────┘    └──────────┘        └──────────────┘    └───────────┘
typ     └─────┘  └──────────────┘   └──────────┘        └──────────────┘   └───────────┘
349    (eq.symm ▸ (mul_dvd_mul_left a $ lcm_dvd
id        └───┘   └──────────────┘    └─────┘
src       └───┘   └──────────────┘     └─────┘
typ       └───┘   └──────────────┘    └─────┘
350      ((mul_dvd_mul_iff_left ha).1 $ eq ▸ dvd_lcm_left _ _)
id         └──────────────────┘ └┘         └──────────┘
src        └──────────────────┘            └──────────┘
typ        └──────────────────┘ └┘         └──────────┘
doc        └──────────────────┘
351      ((mul_dvd_mul_iff_left ha).1 $ eq ▸ dvd_lcm_right _ _)))
id         └──────────────────┘ └┘         └───────────┘
src        └──────────────────┘            └───────────┘
typ        └──────────────────┘ └┘         └───────────┘
doc        └──────────────────┘
352  
353  @[simp] theorem lcm_mul_right (a b c : α) : lcm (b * a) (c * a) = lcm b c * normalize a :=
id                                              └─┘            └─┘    └───────┘ 
src                                              └─┘                └─┘      └───────┘
typ                                             └─┘            └─┘    └───────┘ 
doc    └──┘
354  by simp only [mul_comm, lcm_mul_left]
id                 └──────┘  └──────────┘
src     └─────────┘└──────┘└┘└──────────┘└─
typ     └─────────┘└──────┘└┘└──────────┘└─
doc     └─────────┘        └┘            └─
txt     └─────────┘        └┘            └─
par     └─────────┘        └┘            └─
pid         └──┘└┘        └┘            
st     └───────────────────────────────────
355  
src  
typ  
doc  
txt  
par  
pid  
st   
356  theorem lcm_eq_left_iff (a b : α) (h : normalize a = a) : lcm a b = a ↔ b ∣ a :=
id                                         └───────┘       └─┘        
src                                         └───────┘         └─┘           
typ                                        └───────┘       └─┘        
357  iff.intro (assume eq, eq ▸ dvd_lcm_right _ _) $
id   └───────┘         └┘  └┘  └───────────┘
src  └───────┘         └┘  └┘  └───────────┘
typ  └───────┘         └┘  └┘  └───────────┘
358    assume hab, dvd_antisymm_of_normalize_eq (normalize_lcm _ _) h (lcm_dvd (dvd_refl a) hab) (dvd_lcm_left _ _)
id            └─┘  └──────────────────────────┘  └───────────┘        └─────┘  └──────┘   └─┘   └──────────┘
src                └──────────────────────────┘  └───────────┘         └─────┘  └──────┘          └──────────┘
typ           └─┘  └──────────────────────────┘  └───────────┘        └─────┘  └──────┘   └─┘   └──────────┘
359  
360  theorem lcm_eq_right_iff (a b : α) (h : normalize b = b) : lcm a b = b ↔ a ∣ b :=
id                                          └───────┘       └─┘        
src                                          └───────┘         └─┘           
typ                                         └───────┘       └─┘        
361  by simpa only [lcm_comm b a] using lcm_eq_left_iff b a h
id                  └──────┘          └─────────────┘   
src     └──────────┘└──────┘  └──────┘└─────────────┘   
typ     └──────────┘└──────┘└──────┘└─────────────┘
doc     └──────────┘          └──────┘                  
txt     └──────────┘          └──────┘                  
par     └──────────┘          └──────┘                  
pid          └──┘└┘          └────┘                  
st     └──────────────────────────────────────────────────────
362  
src  
typ  
doc  
txt  
par  
pid  
st   
363  theorem lcm_dvd_lcm_mul_left (m n k : α) : lcm m n ∣ lcm (k * m) n :=
id                                             └─┘    └─┘      
src                                             └─┘      └─┘    
typ                                            └─┘    └─┘      
364  lcm_dvd_lcm (dvd_mul_left _ _) (dvd_refl _)
id   └─────────┘  └──────────┘       └──────┘
src  └─────────┘  └──────────┘       └──────┘
typ  └─────────┘  └──────────┘       └──────┘
365  
366  theorem lcm_dvd_lcm_mul_right (m n k : α) : lcm m n ∣ lcm (m * k) n :=
id                                              └─┘    └─┘      
src                                              └─┘      └─┘    
typ                                             └─┘    └─┘      
367  lcm_dvd_lcm (dvd_mul_right _ _) (dvd_refl _)
id   └─────────┘  └───────────┘       └──────┘
src  └─────────┘  └───────────┘       └──────┘
typ  └─────────┘  └───────────┘       └──────┘
368  
369  theorem lcm_dvd_lcm_mul_left_right (m n k : α) : lcm m n ∣ lcm m (k * n) :=
id                                                   └─┘    └─┘     
src                                                   └─┘      └─┘      
typ                                                  └─┘    └─┘     
370  lcm_dvd_lcm (dvd_refl _) (dvd_mul_left _ _)
id   └─────────┘  └──────┘     └──────────┘
src  └─────────┘  └──────┘     └──────────┘
typ  └─────────┘  └──────┘     └──────────┘
371  
372  theorem lcm_dvd_lcm_mul_right_right (m n k : α) : lcm m n ∣ lcm m (n * k) :=
id                                                    └─┘    └─┘     
src                                                    └─┘      └─┘      
typ                                                   └─┘    └─┘     
373  lcm_dvd_lcm (dvd_refl _) (dvd_mul_right _ _)
id   └─────────┘  └──────┘     └───────────┘
src  └─────────┘  └──────┘     └───────────┘
typ  └─────────┘  └──────┘     └───────────┘
374  
375  end lcm
376  
377  end gcd_domain
378  
379  namespace int
380  
381  section normalization_domain
382  
383  instance : normalization_domain ℤ :=
id              └──────────────────┘ 
src             └──────────────────┘ 
typ             └──────────────────┘ 
doc             └──────────────────┘
384  { norm_unit      := λa:ℤ, if 0 ≤ a then 1 else -1,
id                                               
src                                               
typ                                              
385    norm_unit_zero := if_pos (le_refl _),
id                       └────┘  └─────┘
src                      └────┘  └─────┘
typ                      └────┘  └─────┘
386    norm_unit_mul  := assume a b hna hnb,
id                                └─┘ └─┘
typ                               └─┘ └─┘
387    begin
st     └─────
388      by_cases ha : 0 ≤ a; by_cases hb : 0 ≤ b; simp [ha, hb],
id                                                    └┘  └┘
src      └───────┘  └───┘   └───────┘  └───┘    └────┘  └┘  
typ      └───────┘  └───┘  └───────┘  └───┘   └────┘└┘└┘└┘
doc      └───────┘  └───┘    └───────┘  └───┘    └────┘  └┘  
txt      └───────┘  └───┘    └───────┘  └───┘    └────┘  └┘  
par      └───────┘  └───┘    └───────┘  └───┘    └────┘  └┘  
pid                └───┘              └───┘          └┘  
st   ──────────────────────────────────────────────────────────┘└─
389      exact if_pos (mul_nonneg ha hb),
id             └────┘  └────────┘ └┘ └┘
src      └────┘└────┘ └────────┘    
typ      └────┘└────┘ └────────┘└┘└┘
doc      └────┘                     
txt      └────┘                     
par      └────┘                     
pid                                
st   ──────────────────────────────────┘└─
390      exact if_neg (assume h, hb $ nonneg_of_mul_nonneg_left h $ lt_of_le_of_ne ha hna.symm),
id             └────┘            └┘   └───────────────────────┘     └────────────┘ └┘ └──────┘
src      └────┘└────┘       └──┘   └───────────────────────┘  └────────────┘  └──────┘
typ      └────┘└────┘       └──┘└┘ └───────────────────────┘  └────────────┘└┘└──────┘
doc      └────┘             └──┘                                                      
txt      └────┘             └──┘                                                      
par      └────┘             └──┘                                                      
pid                        └──┘                                                      
st   ─────────────────────────────────────────────────────────────────────────────────────────┘└─
391      exact if_neg (assume h, ha $ nonneg_of_mul_nonneg_right h $ lt_of_le_of_ne hb hnb.symm),
id             └────┘            └┘   └────────────────────────┘     └────────────┘ └┘ └──────┘
src      └────┘└────┘       └──┘   └────────────────────────┘  └────────────┘  └──────┘
typ      └────┘└────┘       └──┘└┘ └────────────────────────┘  └────────────┘└┘└──────┘
doc      └────┘             └──┘                                                       
txt      └────┘             └──┘                                                       
par      └────┘             └──┘                                                       
pid                        └──┘                                                       
st   ──────────────────────────────────────────────────────────────────────────────────────────┘└─
392      exact if_pos (mul_nonneg_of_nonpos_of_nonpos (le_of_not_ge ha) (le_of_not_ge hb))
id             └────┘  └────────────────────────────┘               └┘   └──────────┘ └┘
src      └────┘└────┘ └────────────────────────────┘               └┘ └──────────┘  └──
typ      └────┘└────┘ └────────────────────────────┘             └┘└┘ └──────────┘└┘└──
doc      └────┘                                                    └┘               └──
txt      └────┘                                                    └┘               └──
par      └────┘                                                    └┘               └──
pid                                                               └┘               └┘
st   ──────────────────────────────────────────────────────────────────────────────────────
393    end,
src  ─┘
typ  ─┘
doc  ─┘
txt  ─┘
par  ─┘
pid  ─┘
st   ─┘└─┘
394    norm_unit_coe_units := assume u, (units_eq_one_or u).elim
id                                      └─────────────┘  └──┘
src                                      └─────────────┘   └──┘
typ                                     └─────────────┘  └──┘
395      (assume eq, eq.symm ▸ if_pos zero_le_one)
id               └┘  └┘└───┘  └────┘ └─────────┘
src              └┘  └┘└───┘  └────┘ └─────────┘
typ              └┘  └┘└───┘  └────┘ └─────────┘
396      (assume eq, eq.symm ▸ if_neg (not_le_of_gt $ show (-1:ℤ) < 0, by simp [@neg_lt ℤ _ 1 0])),
id               └┘  └┘└───┘  └────┘  └──────────┘                           └────┘
src              └┘  └┘└───┘  └────┘  └──────────┘                    └────┘ └────┘ └─────┘
typ              └┘  └┘└───┘  └────┘  └──────────┘                    └────┘ └────┘ └─────┘
doc                                                                       └────┘        └─────┘
txt                                                                       └────┘        └─────┘
par                                                                       └────┘        └─────┘
pid                                                                                   └─────┘
st                                                                       └─────────────────────┘
397    .. (infer_instance : integral_domain ℤ) }
id         └────────────┘   └─────────────┘ 
src        └────────────┘   └─────────────┘ 
typ        └────────────┘   └─────────────┘ 
doc        └────────────┘
398  
399  lemma normalize_of_nonneg {z : ℤ} (h : 0 ≤ z) : normalize z = z :=
id                                                └───────┘   
src                                                └───────┘   
typ                                               └───────┘   
400  show z * ↑(ite _ _ _) = z, by rw [if_pos h, units.coe_one, mul_one]
id           └─┘                  └────┘   └───────────┘  └─────┘
src           └─┘               └──┘└────┘ └┘└───────────┘└┘└─────┘└─
typ          └─┘              └──┘└────┘└┘└───────────┘└┘└─────┘└─
doc                                └──┘       └┘             └┘       └─
txt                                └──┘       └┘             └┘       └─
par                                └──┘       └┘             └┘       └─
pid                                  └┘       └┘             └┘       
st                                └───────────┘└─────────────┘└───────┘
401  
src  
typ  
doc  
txt  
par  
pid  
st   
402  lemma normalize_of_neg {z : ℤ} (h : z < 0) : normalize z = -z :=
id                                             └───────┘   
src                                             └───────┘    
typ                                            └───────┘   
403  show z * ↑(ite _ _ _) = -z, by rw [if_neg (not_le_of_gt h), units.coe_neg, units.coe_one, mul_neg_one]
id           └─┘                  └────┘  └──────────┘    └───────────┘  └───────────┘  └─────────┘
src           └─┘               └──┘└────┘ └──────────┘ └─┘└───────────┘└┘└───────────┘└┘└─────────┘└─
typ          └─┘              └──┘└────┘ └──────────┘└─┘└───────────┘└┘└───────────┘└┘└─────────┘└─
doc                                 └──┘                    └─┘└───────────┘└┘             └┘└─────────┘└─
txt                                 └──┘                    └─┘             └┘             └┘           └─
par                                 └──┘                    └─┘             └┘             └┘           └─
pid                                   └┘                    └─┘             └┘             └┘           
st                                 └──────────────────────────┘└─────────────┘└─────────────┘└───────────┘
404  
src  
typ  
doc  
txt  
par  
pid  
st   
405  lemma normalize_coe_nat (n : ℕ) : normalize (n : ℤ) = n :=
id                                    └───────┘        
src                                   └───────┘        
typ                                   └───────┘        
406  normalize_of_nonneg (coe_nat_le_coe_nat_of_le $ nat.zero_le n)
id   └─────────────────┘  └──────────────────────┘   └─────────┘ 
src  └─────────────────┘  └──────────────────────┘   └─────────┘
typ  └─────────────────┘  └──────────────────────┘   └─────────┘ 
407  
408  theorem coe_nat_abs_eq_normalize (z : ℤ) : (z.nat_abs : ℤ) = normalize z :=
id                                              └──────┘      └───────┘ 
src                                              └──────┘      └───────┘
typ                                             └──────┘      └───────┘ 
409  begin
st   └─────
410    by_cases 0 ≤ z,
id                 
src    └─────────┘
typ    └─────────┘
doc    └─────────┘ 
txt    └─────────┘ 
par    └─────────┘ 
pid            └─┘ 
st   ───────────────┘└─
411    { simp [nat_abs_of_nonneg h, normalize_of_nonneg h] },
id             └───────────────┘   └─────────────────┘ 
src      └────┘└───────────────┘ └┘└─────────────────┘ └┘
typ      └────┘└───────────────┘└┘└─────────────────┘└┘
doc      └────┘                  └┘                    └┘
txt      └────┘                  └┘                    └┘
par      └────┘                  └┘                    └┘
pid                            └┘                    
st   ───┘└────────────────────────────────────────────────┘└┘
412    { simp [of_nat_nat_abs_of_nonpos (le_of_not_ge h), normalize_of_neg (lt_of_not_ge h)] }
id             └──────────────────────┘  └──────────┘    └──────────────┘  └──────────┘ 
src      └────┘└──────────────────────┘ └──────────┘ └─┘└──────────────┘ └──────────┘ └─┘
typ      └────┘└──────────────────────┘ └──────────┘└─┘└──────────────┘ └──────────┘└─┘
doc      └────┘                                      └─┘                              └─┘
txt      └────┘                                      └─┘                              └─┘
par      └────┘                                      └─┘                              └─┘
pid                                                └─┘                              └┘
st   ───────────────────────────────────────────────────────────────────────────────────────┘└─
413  end
st   ──┘
414  
415  end normalization_domain
416  
417  /-- ℤ specific version of least common multiple. -/
418  def lcm (i j : ℤ) : ℕ := nat.lcm (nat_abs i) (nat_abs j)
id                          └─────┘  └─────┘    └─────┘ 
src                         └─────┘  └─────┘     └─────┘
typ                         └─────┘  └─────┘    └─────┘ 
419  
420  theorem lcm_def (i j : ℤ) : lcm i j = nat.lcm (nat_abs i) (nat_abs j) := rfl
id                              └─┘    └─────┘  └─────┘    └─────┘      └─┘
src                             └─┘      └─────┘  └─────┘     └─────┘       └─┘
typ                             └─┘    └─────┘  └─────┘    └─────┘      └─┘
doc                              └─┘
421  
422  section gcd_domain
423  
424  theorem gcd_dvd_left (i j : ℤ) : (gcd i j : ℤ) ∣ i :=
id                                    └─┘        
src                                   └─┘         
typ                                   └─┘        
425  dvd_nat_abs.mp $ coe_nat_dvd.mpr $ nat.gcd_dvd_left _ _
id   └─────────┘└─┘   └─────────┘└──┘   └──────────────┘
src  └─────────┘└─┘   └─────────┘└──┘   └──────────────┘
typ  └─────────┘└─┘   └─────────┘└──┘   └──────────────┘
426  
427  theorem gcd_dvd_right (i j : ℤ) : (gcd i j : ℤ) ∣ j :=
id                                     └─┘        
src                                    └─┘         
typ                                    └─┘        
428  dvd_nat_abs.mp $ coe_nat_dvd.mpr $ nat.gcd_dvd_right _ _
id   └─────────┘└─┘   └─────────┘└──┘   └───────────────┘
src  └─────────┘└─┘   └─────────┘└──┘   └───────────────┘
typ  └─────────┘└─┘   └─────────┘└──┘   └───────────────┘
429  
430  theorem dvd_gcd {i j k : ℤ} (h1 : k ∣ i) (h2 : k ∣ j) : k ∣ gcd i j :=
id                                                      └─┘  
src                                                          └─┘
typ                                                     └─┘  
431  nat_abs_dvd.1 $ coe_nat_dvd.2 $ nat.dvd_gcd (nat_abs_dvd_abs_iff.2 h1) (nat_abs_dvd_abs_iff.2 h2)
id   └─────────┘    └─────────┘    └─────────┘  └─────────────────┘  └┘   └─────────────────┘  └┘
src  └─────────┘    └─────────┘    └─────────┘  └─────────────────┘       └─────────────────┘
typ  └─────────┘    └─────────┘    └─────────┘  └─────────────────┘  └┘   └─────────────────┘  └┘
432  
433  theorem gcd_mul_lcm (i j : ℤ) : gcd i j * lcm i j = nat_abs (i * j) :=
id                                  └─┘    └─┘    └─────┘    
src                                 └─┘      └─┘      └─────┘    
typ                                 └─┘    └─┘    └─────┘    
doc                                            └─┘
434  by rw [int.gcd, int.lcm, nat.gcd_mul_lcm, nat_abs_mul]
id          └─────┘  └─────┘  └─────────────┘  └─────────┘
src     └──┘└─────┘└┘└─────┘└┘└─────────────┘└┘└─────────┘└─
typ     └──┘└─────┘└┘└─────┘└┘└─────────────┘└┘└─────────┘└─
doc     └──┘       └┘└─────┘└┘               └┘           └─
txt     └──┘       └┘       └┘               └┘           └─
par     └──┘       └┘       └┘               └┘           └─
pid       └┘       └┘       └┘               └┘           
st     └──────────┘└───────┘└───────────────┘└───────────┘
435  
src  
typ  
doc  
txt  
par  
pid  
st   
436  instance : gcd_domain ℤ :=
id              └────────┘ 
src             └────────┘ 
typ             └────────┘ 
doc             └────────┘
437  { gcd            := λa b, int.gcd a b,
id                           └─────┘  
src                            └─────┘
typ                          └─────┘  
438    lcm            := λa b, int.lcm a b,
id                           └─────┘  
src                            └─────┘
typ                          └─────┘  
doc                            └─────┘
439    gcd_dvd_left   := assume a b, int.gcd_dvd_left _ _,
id                                 └──────────────┘
src                                  └──────────────┘
typ                                └──────────────┘
440    gcd_dvd_right  := assume a b, int.gcd_dvd_right _ _,
id                                 └───────────────┘
src                                  └───────────────┘
typ                                └───────────────┘
441    dvd_gcd        := assume a b c, dvd_gcd,
id                                  └─────┘
src                                    └─────┘
typ                                 └─────┘
442    normalize_gcd  := assume a b, normalize_coe_nat _,
id                                 └───────────────┘
src                                  └───────────────┘
typ                                └───────────────┘
443    gcd_mul_lcm    := by intros; rw [← int.coe_nat_mul, gcd_mul_lcm, coe_nat_abs_eq_normalize],
id                                        └─────────────┘  └─────────┘  └──────────────────────┘
src                         └────┘  └────┘└─────────────┘└┘└─────────┘└┘└──────────────────────┘
typ                         └────┘  └────┘└─────────────┘└┘└─────────┘└┘└──────────────────────┘
doc                         └────┘  └────┘               └┘           └┘                        
txt                         └────┘  └────┘               └┘           └┘                        
par                         └────┘  └────┘               └┘           └┘                        
pid                                   └──┘               └┘           └┘                        
st                         └───────────┘└───────────────┘└───────────┘└────────────────────────┘
444    lcm_zero_left  := assume a, coe_nat_eq_zero.2 $ nat.lcm_zero_left _,
id                                └─────────────┘    └───────────────┘
src                                └─────────────┘    └───────────────┘
typ                               └─────────────┘    └───────────────┘
445    lcm_zero_right := assume a, coe_nat_eq_zero.2 $ nat.lcm_zero_right _,
id                                └─────────────┘    └────────────────┘
src                                └─────────────┘    └────────────────┘
typ                               └─────────────┘    └────────────────┘
446    .. int.normalization_domain }
id        └──────────────────────┘
src       └──────────────────────┘
typ       └──────────────────────┘
447  
448  lemma coe_gcd (i j : ℤ) : ↑(int.gcd i j) = gcd_domain.gcd i j := rfl
id                             └─────┘     └────────────┘      └─┘
src                            └─────┘       └────────────┘        └─┘
typ                            └─────┘     └────────────┘      └─┘
449  lemma coe_lcm (i j : ℤ) : ↑(int.lcm i j) = gcd_domain.lcm i j := rfl
id                             └─────┘     └────────────┘      └─┘
src                            └─────┘       └────────────┘        └─┘
typ                            └─────┘     └────────────┘      └─┘
doc                              └─────┘
450  
451  lemma nat_abs_gcd (i j : ℤ) : nat_abs (gcd_domain.gcd i j) = int.gcd i j := rfl
id                                └─────┘  └────────────┘     └─────┘      └─┘
src                               └─────┘  └────────────┘       └─────┘        └─┘
typ                               └─────┘  └────────────┘     └─────┘      └─┘
452  lemma nat_abs_lcm (i j : ℤ) : nat_abs (gcd_domain.lcm i j) = int.lcm i j := rfl
id                                └─────┘  └────────────┘     └─────┘      └─┘
src                               └─────┘  └────────────┘       └─────┘        └─┘
typ                               └─────┘  └────────────┘     └─────┘      └─┘
doc                                                               └─────┘
453  
454  end gcd_domain
455  
456  theorem gcd_comm (i j : ℤ) : gcd i j = gcd j i := nat.gcd_comm _ _
id                               └─┘    └─┘      └──────────┘
src                              └─┘      └─┘        └──────────┘
typ                              └─┘    └─┘      └──────────┘
457  
458  theorem gcd_assoc (i j k : ℤ) : gcd (gcd i j) k = gcd i (gcd j k) := nat.gcd_assoc _ _ _
id                                  └─┘  └─┘      └─┘   └─┘       └───────────┘
src                                 └─┘  └─┘         └─┘    └─┘         └───────────┘
typ                                 └─┘  └─┘      └─┘   └─┘       └───────────┘
459  
460  @[simp] theorem gcd_self (i : ℤ) : gcd i i = nat_abs i := by simp [gcd]
id                                     └─┘    └─────┘              └─┘
src                                    └─┘      └─────┘         └────┘└─┘└─
typ                                    └─┘    └─────┘        └────┘└─┘└─
doc    └──┘                                                       └────┘   └─
txt                                                               └────┘   └─
par                                                               └────┘   └─
pid                                                                      
st                                                               └───────────
461  
src  
typ  
doc  
txt  
par  
pid  
st   
462  @[simp] theorem gcd_zero_left (i : ℤ) : gcd 0 i = nat_abs i := by simp [gcd]
id                                          └─┘     └─────┘              └─┘
src                                         └─┘      └─────┘         └────┘└─┘└─
typ                                         └─┘     └─────┘        └────┘└─┘└─
doc    └──┘                                                            └────┘   └─
txt                                                                    └────┘   └─
par                                                                    └────┘   └─
pid                                                                           
st                                                                    └───────────
463  
src  
typ  
doc  
txt  
par  
pid  
st   
464  @[simp] theorem gcd_zero_right (i : ℤ) : gcd i 0 = nat_abs i := by simp [gcd]
id                                           └─┘     └─────┘              └─┘
src                                          └─┘      └─────┘         └────┘└─┘└─
typ                                          └─┘     └─────┘        └────┘└─┘└─
doc    └──┘                                                             └────┘   └─
txt                                                                     └────┘   └─
par                                                                     └────┘   └─
pid                                                                            
st                                                                     └───────────
465  
src  
typ  
doc  
txt  
par  
pid  
st   
466  @[simp] theorem gcd_one_left (i : ℤ) : gcd 1 i = 1 := nat.gcd_one_left _
id                                         └─┘          └──────────────┘
src                                        └─┘           └──────────────┘
typ                                        └─┘          └──────────────┘
doc    └──┘
467  
468  @[simp] theorem gcd_one_right (i : ℤ) : gcd i 1 = 1 := nat.gcd_one_right _
id                                          └─┘          └───────────────┘
src                                         └─┘           └───────────────┘
typ                                         └─┘          └───────────────┘
doc    └──┘
469  
470  theorem gcd_mul_left (i j k : ℤ) : gcd (i * j) (i * k) = nat_abs i * gcd j k :=
id                                     └─┘            └─────┘   └─┘  
src                                    └─┘                └─────┘    └─┘
typ                                    └─┘            └─────┘   └─┘  
471  by simp [(int.coe_nat_eq_coe_nat_iff _ _).symm, coe_gcd, coe_nat_abs_eq_normalize]
id             └────────────────────────┘            └─────┘  └──────────────────────┘
src     └────┘ └────────────────────────┘└──────────┘└─────┘└┘└──────────────────────┘└─
typ     └────┘ └────────────────────────┘└──────────┘└─────┘└┘└──────────────────────┘└─
doc     └────┘                           └──────────┘       └┘                        └─
txt     └────┘                           └──────────┘       └┘                        └─
par     └────┘                           └──────────┘       └┘                        └─
pid                                    └──────────┘       └┘                        
st     └────────────────────────────────────────────────────────────────────────────────
472  
src  
typ  
doc  
txt  
par  
pid  
st   
473  theorem gcd_mul_right (i j k : ℤ) : gcd (i * j) (k * j) = gcd i k * nat_abs j :=
id                                      └─┘            └─┘    └─────┘ 
src                                     └─┘                └─┘      └─────┘
typ                                     └─┘            └─┘    └─────┘ 
474  by simp [(int.coe_nat_eq_coe_nat_iff _ _).symm, coe_gcd, coe_nat_abs_eq_normalize]
id             └────────────────────────┘            └─────┘  └──────────────────────┘
src     └────┘ └────────────────────────┘└──────────┘└─────┘└┘└──────────────────────┘└─
typ     └────┘ └────────────────────────┘└──────────┘└─────┘└┘└──────────────────────┘└─
doc     └────┘                           └──────────┘       └┘                        └─
txt     └────┘                           └──────────┘       └┘                        └─
par     └────┘                           └──────────┘       └┘                        └─
pid                                    └──────────┘       └┘                        
st     └────────────────────────────────────────────────────────────────────────────────
475  
src  
typ  
doc  
txt  
par  
pid  
st   
476  theorem gcd_pos_of_non_zero_left {i : ℤ} (j : ℤ) (i_non_zero : i ≠ 0) : 0 < gcd i j :=
id                                                                          └─┘  
src                                                                          └─┘
typ                                                                         └─┘  
477  nat.gcd_pos_of_pos_left (nat_abs j) (nat_abs_pos_of_ne_zero i_non_zero)
id   └─────────────────────┘  └─────┘    └────────────────────┘ └────────┘
src  └─────────────────────┘  └─────┘     └────────────────────┘
typ  └─────────────────────┘  └─────┘    └────────────────────┘ └────────┘
478  
479  theorem gcd_pos_of_non_zero_right (i : ℤ) {j : ℤ} (j_non_zero : j ≠ 0) : 0 < gcd i j :=
id                                                                           └─┘  
src                                                                           └─┘
typ                                                                          └─┘  
480  nat.gcd_pos_of_pos_right (nat_abs i) (nat_abs_pos_of_ne_zero j_non_zero)
id   └──────────────────────┘  └─────┘    └────────────────────┘ └────────┘
src  └──────────────────────┘  └─────┘     └────────────────────┘
typ  └──────────────────────┘  └─────┘    └────────────────────┘ └────────┘
481  
482  theorem gcd_eq_zero_iff {i j : ℤ} : gcd i j = 0 ↔ i = 0 ∧ j = 0 :=
id                                      └─┘             
src                                     └─┘                 
typ                                     └─┘             
483  by rw [← int.coe_nat_eq_coe_nat_iff, int.coe_nat_zero, coe_gcd, gcd_eq_zero_iff]
id            └────────────────────────┘  └──────────────┘  └─────┘  └─────────────┘
src     └────┘└────────────────────────┘└┘└──────────────┘└┘└─────┘└┘└─────────────┘└─
typ     └────┘└────────────────────────┘└┘└──────────────┘└┘└─────┘└┘└─────────────┘└─
doc     └────┘                          └┘                └┘       └┘               └─
txt     └────┘                          └┘                └┘       └┘               └─
par     └────┘                          └┘                └┘       └┘               └─
pid       └──┘                          └┘                └┘       └┘               
st     └───────────────────────────────┘└────────────────┘└───────┘└───────────────┘
484  
src  
typ  
doc  
txt  
par  
pid  
st   
485  theorem gcd_div {i j k : ℤ} (H1 : k ∣ i) (H2 : k ∣ j) :
id                                                
src                                                 
typ                                               
486    gcd (i / k) (j / k) = gcd i j / nat_abs k :=
id     └─┘            └─┘    └─────┘ 
src    └─┘                └─┘      └─────┘
typ    └─┘            └─┘    └─────┘ 
487  by rw [gcd, nat_abs_div i k H1, nat_abs_div j k H2];
id          └─┘  └─────────┘   └┘  └─────────┘   └┘
src     └──┘└─┘└┘└─────────┘    └┘└─────────┘    
typ     └──┘└─┘└┘└─────────┘└┘└┘└─────────┘└┘
doc     └──┘   └┘               └┘               
txt     └──┘   └┘               └┘               
par     └──┘   └┘               └┘               
pid       └┘   └┘               └┘               
st     └──────┘└──────────────────┘└──────────────────┘└─
488  exact nat.gcd_div (nat_abs_dvd_abs_iff.mpr H1) (nat_abs_dvd_abs_iff.mpr H2)
id         └─────────┘                          └┘   └─────────────────────┘ └┘
src  └────┘└─────────┘                          └┘ └─────────────────────┘  └─
typ  └────┘└─────────┘                        └┘└┘ └─────────────────────┘└┘└─
doc  └────┘                                     └┘                          └─
txt  └────┘                                     └┘                          └─
par  └────┘                                     └┘                          └─
pid                                            └┘                          
st   ────────────────────────────────────────────────────────────────────────────
489  
src  
typ  
doc  
txt  
par  
pid  
st   
490  theorem gcd_dvd_gcd_of_dvd_left {i k : ℤ} (j : ℤ) (H : i ∣ k) : gcd i j ∣ gcd k j :=
id                                                              └─┘    └─┘  
src                                                               └─┘      └─┘
typ                                                             └─┘    └─┘  
491  int.coe_nat_dvd.1 $ dvd_gcd (dvd.trans (gcd_dvd_left i j) H) (gcd_dvd_right i j)
id   └─────────────┘    └─────┘  └───────┘  └──────────┘       └───────────┘  
src  └─────────────┘    └─────┘  └───────┘  └──────────┘          └───────────┘
typ  └─────────────┘    └─────┘  └───────┘  └──────────┘       └───────────┘  
492  
493  theorem gcd_dvd_gcd_of_dvd_right {i k : ℤ} (j : ℤ) (H : i ∣ k) : gcd j i ∣ gcd j k :=
id                                                               └─┘    └─┘  
src                                                                └─┘      └─┘
typ                                                              └─┘    └─┘  
494  int.coe_nat_dvd.1 $ dvd_gcd (gcd_dvd_left j i) (dvd.trans (gcd_dvd_right j i) H)
id   └─────────────┘    └─────┘  └──────────┘     └───────┘  └───────────┘    
src  └─────────────┘    └─────┘  └──────────┘       └───────┘  └───────────┘
typ  └─────────────┘    └─────┘  └──────────┘     └───────┘  └───────────┘    
495  
496  theorem gcd_dvd_gcd_mul_left (i j k : ℤ) : gcd i j ∣ gcd (k * i) j :=
id                                             └─┘    └─┘      
src                                            └─┘      └─┘    
typ                                            └─┘    └─┘      
497  gcd_dvd_gcd_of_dvd_left _ (dvd_mul_left _ _)
id   └─────────────────────┘    └──────────┘
src  └─────────────────────┘    └──────────┘
typ  └─────────────────────┘    └──────────┘
498  
499  theorem gcd_dvd_gcd_mul_right (i j k : ℤ) : gcd i j ∣ gcd (i * k) j :=
id                                              └─┘    └─┘      
src                                             └─┘      └─┘    
typ                                             └─┘    └─┘      
500  gcd_dvd_gcd_of_dvd_left _ (dvd_mul_right _ _)
id   └─────────────────────┘    └───────────┘
src  └─────────────────────┘    └───────────┘
typ  └─────────────────────┘    └───────────┘
501  
502  theorem gcd_dvd_gcd_mul_left_right (i j k : ℤ) : gcd i j ∣ gcd i (k * j) :=
id                                                   └─┘    └─┘     
src                                                  └─┘      └─┘      
typ                                                  └─┘    └─┘     
503  gcd_dvd_gcd_of_dvd_right _ (dvd_mul_left _ _)
id   └──────────────────────┘    └──────────┘
src  └──────────────────────┘    └──────────┘
typ  └──────────────────────┘    └──────────┘
504  
505  theorem gcd_dvd_gcd_mul_right_right (i j k : ℤ) : gcd i j ∣ gcd i (j * k) :=
id                                                    └─┘    └─┘     
src                                                   └─┘      └─┘      
typ                                                   └─┘    └─┘     
506  gcd_dvd_gcd_of_dvd_right _ (dvd_mul_right _ _)
id   └──────────────────────┘    └───────────┘
src  └──────────────────────┘    └───────────┘
typ  └──────────────────────┘    └───────────┘
507  
508  theorem gcd_eq_left {i j : ℤ} (H : i ∣ j) : gcd i j = nat_abs i :=
id                                           └─┘    └─────┘ 
src                                            └─┘      └─────┘
typ                                          └─┘    └─────┘ 
509  nat.dvd_antisymm (by unfold gcd; exact nat.gcd_dvd_left _ _)
id   └──────────────┘                       └──────────────┘
src  └──────────────┘     └────────┘  └────┘└──────────────┘└──┘
typ  └──────────────┘     └────────┘  └────┘└──────────────┘└──┘
doc                       └────────┘  └────┘                └──┘
txt                       └────────┘  └────┘                └──┘
par                       └────────┘  └────┘                └──┘
pid                             └──┘                       └──┘
st                       └─────────────────────────────────────┘
510                   (by unfold gcd; exact nat.dvd_gcd (dvd_refl _) (nat_abs_dvd_abs_iff.mpr H))
id                                          └─────────┘  └──────┘     └─────────────────────┘ 
src                       └────────┘  └────┘└─────────┘ └──────┘└──┘ └─────────────────────┘ 
typ                       └────────┘  └────┘└─────────┘ └──────┘└──┘ └─────────────────────┘
doc                       └────────┘  └────┘                    └──┘                         
txt                       └────────┘  └────┘                    └──┘                         
par                       └────────┘  └────┘                    └──┘                         
pid                             └──┘                           └──┘                         
st                       └─────────────────────────────────────────────────────────────────────┘
511  
512  theorem gcd_eq_right {i j : ℤ} (H : j ∣ i) : gcd i j = nat_abs j :=
id                                            └─┘    └─────┘ 
src                                             └─┘      └─────┘
typ                                           └─┘    └─────┘ 
513  by rw [gcd_comm, gcd_eq_left H]
id          └──────┘  └─────────┘ 
src     └──┘└──────┘└┘└─────────┘ └─
typ     └──┘└──────┘└┘└─────────┘└─
doc     └──┘        └┘            └─
txt     └──┘        └┘            └─
par     └──┘        └┘            └─
pid       └┘        └┘            
st     └───────────┘└─────────────┘
514  
src  
typ  
doc  
txt  
par  
pid  
st   
515  /- lcm -/
src  ──────────
typ  ──────────
doc  ──────────
txt  ──────────
par  ──────────
pid  ──────────
st   ──────────
516  
src  
typ  
doc  
txt  
par  
pid  
st   
517  theorem lcm_comm (i j : ℤ) : lcm i j = lcm j i :=
id                               └─┘    └─┘  
src                              └─┘      └─┘
typ                              └─┘    └─┘  
doc                               └─┘       └─┘
518  by simp [(int.coe_nat_eq_coe_nat_iff _ _).symm, coe_lcm, lcm_comm]
id             └────────────────────────┘            └─────┘  └──────┘
src     └────┘ └────────────────────────┘└──────────┘└─────┘└┘└──────┘└─
typ     └────┘ └────────────────────────┘└──────────┘└─────┘└┘└──────┘└─
doc     └────┘                           └──────────┘       └┘        └─
txt     └────┘                           └──────────┘       └┘        └─
par     └────┘                           └──────────┘       └┘        └─
pid                                    └──────────┘       └┘        
st     └────────────────────────────────────────────────────────────────
519  
src  
typ  
doc  
txt  
par  
pid  
st   
520  theorem lcm_assoc (i j k : ℤ) : lcm (lcm i j) k = lcm i (lcm j k) :=
id                                  └─┘  └─┘      └─┘   └─┘  
src                                 └─┘  └─┘         └─┘    └─┘
typ                                 └─┘  └─┘      └─┘   └─┘  
doc                                  └─┘  └─┘          └─┘    └─┘
521  by simp [(int.coe_nat_eq_coe_nat_iff _ _).symm, coe_lcm, lcm_assoc]
id             └────────────────────────┘            └─────┘  └───────┘
src     └────┘ └────────────────────────┘└──────────┘└─────┘└┘└───────┘└─
typ     └────┘ └────────────────────────┘└──────────┘└─────┘└┘└───────┘└─
doc     └────┘                           └──────────┘       └┘         └─
txt     └────┘                           └──────────┘       └┘         └─
par     └────┘                           └──────────┘       └┘         └─
pid                                    └──────────┘       └┘         
st     └─────────────────────────────────────────────────────────────────
522  
src  
typ  
doc  
txt  
par  
pid  
st   
523  @[simp] theorem lcm_zero_left (i : ℤ) : lcm 0 i = 0 :=
id                                          └─┘    
src                                         └─┘     
typ                                         └─┘    
doc    └──┘                                  └─┘
524  by simp [(int.coe_nat_eq_coe_nat_iff _ _).symm, coe_lcm]
id             └────────────────────────┘            └─────┘
src     └────┘ └────────────────────────┘└──────────┘└─────┘└─
typ     └────┘ └────────────────────────┘└──────────┘└─────┘└─
doc     └────┘                           └──────────┘       └─
txt     └────┘                           └──────────┘       └─
par     └────┘                           └──────────┘       └─
pid                                    └──────────┘       
st     └──────────────────────────────────────────────────────
525  
src  
typ  
doc  
txt  
par  
pid  
st   
526  @[simp] theorem lcm_zero_right (i : ℤ) : lcm i 0 = 0 :=
id                                           └─┘    
src                                          └─┘     
typ                                          └─┘    
doc    └──┘                                   └─┘
527  by simp [(int.coe_nat_eq_coe_nat_iff _ _).symm, coe_lcm]
id             └────────────────────────┘            └─────┘
src     └────┘ └────────────────────────┘└──────────┘└─────┘└─
typ     └────┘ └────────────────────────┘└──────────┘└─────┘└─
doc     └────┘                           └──────────┘       └─
txt     └────┘                           └──────────┘       └─
par     └────┘                           └──────────┘       └─
pid                                    └──────────┘       
st     └──────────────────────────────────────────────────────
528  
src  
typ  
doc  
txt  
par  
pid  
st   
529  @[simp] theorem lcm_one_left (i : ℤ) : lcm 1 i = nat_abs i :=
id                                         └─┘     └─────┘ 
src                                        └─┘      └─────┘
typ                                        └─┘     └─────┘ 
doc    └──┘                                 └─┘
530  by simp [(int.coe_nat_eq_coe_nat_iff _ _).symm, coe_lcm, coe_nat_abs_eq_normalize]
id             └────────────────────────┘            └─────┘  └──────────────────────┘
src     └────┘ └────────────────────────┘└──────────┘└─────┘└┘└──────────────────────┘└─
typ     └────┘ └────────────────────────┘└──────────┘└─────┘└┘└──────────────────────┘└─
doc     └────┘                           └──────────┘       └┘                        └─
txt     └────┘                           └──────────┘       └┘                        └─
par     └────┘                           └──────────┘       └┘                        └─
pid                                    └──────────┘       └┘                        
st     └────────────────────────────────────────────────────────────────────────────────
531  
src  
typ  
doc  
txt  
par  
pid  
st   
532  @[simp] theorem lcm_one_right (i : ℤ) : lcm i 1 = nat_abs i :=
id                                          └─┘     └─────┘ 
src                                         └─┘      └─────┘
typ                                         └─┘     └─────┘ 
doc    └──┘                                  └─┘
533  by simp [(int.coe_nat_eq_coe_nat_iff _ _).symm, coe_lcm, coe_nat_abs_eq_normalize]
id             └────────────────────────┘            └─────┘  └──────────────────────┘
src     └────┘ └────────────────────────┘└──────────┘└─────┘└┘└──────────────────────┘└─
typ     └────┘ └────────────────────────┘└──────────┘└─────┘└┘└──────────────────────┘└─
doc     └────┘                           └──────────┘       └┘                        └─
txt     └────┘                           └──────────┘       └┘                        └─
par     └────┘                           └──────────┘       └┘                        └─
pid                                    └──────────┘       └┘                        
st     └────────────────────────────────────────────────────────────────────────────────
534  
src  
typ  
doc  
txt  
par  
pid  
st   
535  @[simp] theorem lcm_self (i : ℤ) : lcm i i = nat_abs i :=
id                                     └─┘    └─────┘ 
src                                    └─┘      └─────┘
typ                                    └─┘    └─────┘ 
doc    └──┘                             └─┘
536  by simp [(int.coe_nat_eq_coe_nat_iff _ _).symm, coe_lcm, coe_nat_abs_eq_normalize]
id             └────────────────────────┘            └─────┘  └──────────────────────┘
src     └────┘ └────────────────────────┘└──────────┘└─────┘└┘└──────────────────────┘└─
typ     └────┘ └────────────────────────┘└──────────┘└─────┘└┘└──────────────────────┘└─
doc     └────┘                           └──────────┘       └┘                        └─
txt     └────┘                           └──────────┘       └┘                        └─
par     └────┘                           └──────────┘       └┘                        └─
pid                                    └──────────┘       └┘                        
st     └────────────────────────────────────────────────────────────────────────────────
537  
src  
typ  
doc  
txt  
par  
pid  
st   
538  theorem dvd_lcm_left (i j : ℤ) : i ∣ lcm i j :=
id                                     └─┘  
src                                     └─┘
typ                                    └─┘  
doc                                       └─┘
539  by rw [coe_lcm]; exact dvd_lcm_left _ _
id          └─────┘         └──────────┘
src     └──┘└─────┘  └────┘└──────────┘└────
typ     └──┘└─────┘  └────┘└──────────┘└────
doc     └──┘         └────┘            └────
txt     └──┘         └────┘            └────
par     └──┘         └────┘            └────
pid       └┘                          └──┘
st     └──────────┘└────────────────────────
540  
src  
typ  
doc  
txt  
par  
pid  
st   
541  theorem dvd_lcm_right (i j : ℤ) : j ∣ lcm i j :=
id                                      └─┘  
src                                      └─┘
typ                                     └─┘  
doc                                        └─┘
542  by rw [coe_lcm]; exact dvd_lcm_right _ _
id          └─────┘         └───────────┘
src     └──┘└─────┘  └────┘└───────────┘└────
typ     └──┘└─────┘  └────┘└───────────┘└────
doc     └──┘         └────┘             └────
txt     └──┘         └────┘             └────
par     └──┘         └────┘             └────
pid       └┘                           └──┘
st     └──────────┘└─────────────────────────
543  
src  
typ  
doc  
txt  
par  
pid  
st   
544  theorem lcm_dvd {i j k : ℤ}  : i ∣ k → j ∣ k → (lcm i j : ℤ) ∣ k :=
id                                            └─┘        
src                                               └─┘         
typ                                           └─┘        
doc                                                  └─┘
545  by rw [coe_lcm]; exact lcm_dvd
id          └─────┘         └─────┘
src     └──┘└─────┘  └────┘└─────┘
typ     └──┘└─────┘  └────┘└─────┘
doc     └──┘         └────┘       
txt     └──┘         └────┘       
par     └──┘         └────┘       
pid       └┘                     
st     └──────────┘└───────────────
546  
src  
typ  
doc  
txt  
par  
pid  
st   
547  end int
548  
549  theorem irreducible_iff_nat_prime : ∀(a : ℕ), irreducible a ↔ nat.prime a
id                                               └─────────┘   └───────┘ 
src                                               └─────────┘    └───────┘
typ                                              └─────────┘   └───────┘ 
doc                                                └─────────┘     └───────┘
550  | 0 := by simp [nat.not_prime_zero]
id                   └────────────────┘
src            └────┘└────────────────┘└┘
typ            └────┘└────────────────┘└┘
doc            └────┘                  └┘
txt            └────┘                  └┘
par            └────┘                  └┘
pid                                  
st            └─────────────────────────┘
551  | 1 := by simp [nat.prime, one_lt_two]
id                   └───────┘  └────────┘
src            └────┘└───────┘└┘└────────┘└┘
typ            └────┘└───────┘└┘└────────┘└┘
doc            └────┘└───────┘└┘          └┘
txt            └────┘         └┘          └┘
par            └────┘         └┘          └┘
pid                         └┘          
st            └────────────────────────────┘
552  | (n + 2) :=
id       
src       
typ      
553    have h₁ : ¬n + 2 = 1, from dec_trivial,
id                             └─────────┘
src                            └─────────┘
typ                            └─────────┘
doc                               └─────────┘
554    begin
st     └─────
555      simp [h₁, nat.prime, irreducible, (≥), nat.le_add_left 2 n, (∣)],
id             └┘  └───────┘  └─────────┘      └─────────────┘   
src      └────┘  └┘└───────┘└┘└─────────┘└┘└──┘└─────────────┘└─┘ └┘ └─┘
typ      └────┘└┘└┘└───────┘└┘└─────────┘└┘└──┘└─────────────┘└─┘└┘ └─┘
doc      └────┘  └┘└───────┘└┘└─────────┘└┘ └──┘               └─┘ └┘ └─┘
txt      └────┘  └┘         └┘           └┘ └──┘               └─┘ └┘ └─┘
par      └────┘  └┘         └┘           └┘ └──┘               └─┘ └┘ └─┘
pid            └┘         └┘           └┘ └──┘               └─┘ └┘ └─┘
st   ───────────────────────────────────────────────────────────────────┘└─
556      refine forall_congr (assume a, forall_congr $ assume b, forall_congr $ assume hab, _),
id                                                               └──────────┘
src      └─────┘                   └──┘                   └──┘└──────────┘       └──────┘
typ      └─────┘                   └──┘                   └──┘└──────────┘       └──────┘
doc      └─────┘                   └──┘                   └──┘                   └──────┘
txt      └─────┘                   └──┘                   └──┘                   └──────┘
par      └─────┘                   └──┘                   └──┘                   └──────┘
pid                               └──┘                   └──┘                   └──────┘
st   ────────────────────────────────────────────────────────────────────────────────────────┘└─
557      by_cases a = 1; simp [h],
id                           
src      └───────┘ └┘  └────┘ 
typ      └───────┘└┘  └────┘
doc      └───────┘  └┘  └────┘ 
txt      └───────┘  └┘  └────┘ 
par      └───────┘  └┘  └────┘ 
pid                       
st   ───────────────────────────┘└─
558      split,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
st   ────────┘└─
559      { assume hb, simpa [hb] using hab.symm },
id                           └┘        └──────┘
src        └───────┘  └─────┘  └──────┘└──────┘
typ        └───────┘  └─────┘└┘└──────┘└──────┘
doc        └───────┘  └─────┘  └──────┘        
txt        └───────┘  └─────┘  └──────┘        
par        └───────┘  └─────┘  └──────┘        
pid        └───────┘         └────┘        
st   ─────┘└───────┘└──────────────────────────┘└┘
560      { assume ha, subst ha,
id                          └┘
src        └───────┘  └────┘
typ        └───────┘  └────┘└┘
doc        └───────┘  └────┘
txt        └───────┘  └────┘
par        └───────┘  └────┘
pid        └───────┘       
st   ──────────────┘└────────┘└─
561        have : n + 2 > 0, from dec_trivial,
id                             └─────────┘
src        └─────┘ └─┘└┘  └───┘└─────────┘
typ        └─────┘└─┘└┘  └───┘└─────────┘
doc        └─────┘  └─┘ └┘  └───┘
txt        └─────┘  └─┘ └┘  └───┘
par        └─────┘  └─┘ └┘  └───┘
pid        └───┘└┘  └─┘   └───┘
st   ─────────────────────┘└────────────────┘└─
562        refine nat.eq_of_mul_eq_mul_left this _,
id                └───────────────────────┘ └──┘
src        └─────┘└───────────────────────┘    └┘
typ        └─────┘└───────────────────────┘└──┘└┘
doc        └─────┘                             └┘
txt        └─────┘                             └┘
par        └─────┘                             └┘
pid                                           └┘
st   ────────────────────────────────────────────┘└─
563        rw [← hab, mul_one] }
id               └─┘  └─────┘
src        └────┘   └┘└─────┘└┘
typ        └────┘└─┘└┘└─────┘└┘
doc        └────┘   └┘       └┘
txt        └────┘   └┘       └┘
par        └────┘   └┘       └┘
pid          └──┘   └┘       
st   ──────────────┘└───────┘└─
564    end
st   ────┘
565  
566  lemma nat.prime_iff_prime {p : ℕ} : p.prime ↔ _root_.prime (p : ℕ) :=
id                                      └────┘  └──────────┘     
src                                      └────┘  └──────────┘      
typ                                     └────┘  └──────────┘     
doc                                       └────┘   └──────────┘
567  ⟨λ hp, ⟨nat.pos_iff_ne_zero.1 hp.pos, mt is_unit_iff_dvd_one.1 hp.not_dvd_one,
id      └┘   └─────────────────┘  └┘└──┘  └┘ └─────────────────┘  └┘└──────────┘
src          └─────────────────┘    └──┘  └┘ └─────────────────┘    └──────────┘
typ     └┘   └─────────────────┘  └┘└──┘  └┘ └─────────────────┘  └┘└──────────┘
568      λ a b, hp.dvd_mul.1⟩,
id            └┘└──────┘
src               └──────┘
typ           └┘└──────┘
569    λ hp, ⟨nat.one_lt_iff_ne_zero_and_ne_one.2 ⟨hp.1, λ h1, hp.2.1 $ h1.symm ▸ is_unit_one⟩,
id       └┘   └───────────────────────────────┘   └┘     └┘  └┘     └┘└───┘  └─────────┘
src           └───────────────────────────────┘                       └───┘  └─────────┘
typ      └┘   └───────────────────────────────┘   └┘     └┘  └┘     └┘└───┘  └─────────┘
570      λ a h, let ⟨b, hab⟩ := h in
id            └─┘    └─┘     
typ           └─┘    └─┘     
571        (hp.2.2 a b (hab ▸ dvd_refl _)).elim
id          └┘            └──────┘    └──┘
src                        └──────┘    └──┘
typ         └┘            └──────┘    └──┘
572          (λ ha, or.inr (nat.dvd_antisymm h ha))
id              └┘  └────┘  └──────────────┘  └┘
src                 └────┘  └──────────────┘
typ             └┘  └────┘  └──────────────┘  └┘
573          (λ hb, or.inl (have hpb : p = b, from nat.dvd_antisymm hb
id              └┘  └────┘                       └──────────────┘ └┘
src                 └────┘                        └──────────────┘
typ             └┘  └────┘                       └──────────────┘ └┘
574              (hab.symm ▸ dvd_mul_left _ _),
id                   └───┘  └──────────┘
src                  └───┘  └──────────┘
typ                  └───┘  └──────────┘
575            (nat.mul_left_inj (show 0 < p, from
id              └──────────────┘          
src             └──────────────┘         
typ             └──────────────┘          
576                nat.pos_of_ne_zero hp.1)).1 $
id                 └────────────────┘ └┘   
src                └────────────────┘      
typ                └────────────────┘ └┘   
577              by rw [hpb, mul_comm, ← hab, hpb, mul_one]))⟩⟩
id                      └─┘  └──────┘    └─┘  └─┘  └─────┘
src                 └──┘   └┘└──────┘└──┘   └┘   └┘└─────┘
typ                 └──┘└─┘└┘└──────┘└──┘└─┘└┘└─┘└┘└─────┘
doc                 └──┘   └┘        └──┘   └┘   └┘       
txt                 └──┘   └┘        └──┘   └┘   └┘       
par                 └──┘   └┘        └──┘   └┘   └┘       
pid                   └┘   └┘        └──┘   └┘   └┘       
st                 └──────┘└────────┘└─────┘└───┘└───────┘
578  
579  lemma nat.prime_iff_prime_int {p : ℕ} : p.prime ↔ _root_.prime (p : ℤ) :=
id                                          └────┘  └──────────┘     
src                                          └────┘  └──────────┘      
typ                                         └────┘  └──────────┘     
doc                                           └────┘   └──────────┘
580  ⟨λ hp, ⟨int.coe_nat_ne_zero_iff_pos.2 hp.pos, mt is_unit_int.1 hp.ne_one,
id      └┘   └─────────────────────────┘  └┘└──┘  └┘ └─────────┘  └┘└─────┘
src          └─────────────────────────┘    └──┘  └┘ └─────────┘    └─────┘
typ     └┘   └─────────────────────────┘  └┘└──┘  └┘ └─────────┘  └┘└─────┘
581    λ a b h, by rw [← int.dvd_nat_abs, int.coe_nat_dvd, int.nat_abs_mul, hp.dvd_mul] at h;
id                    └─────────────┘  └─────────────┘  └─────────────┘
src                └────┘└─────────────┘└┘└─────────────┘└┘└─────────────┘└┘          └────┘
typ             └────┘└─────────────┘└┘└─────────────┘└┘└─────────────┘└┘└────────┘└────┘
doc                └────┘               └┘               └┘               └┘          └────┘
txt                └────┘               └┘               └┘               └┘          └────┘
par                └────┘               └┘               └┘               └┘          └────┘
pid                  └──┘               └┘               └┘               └┘          └───┘
st                └────────────────────┘└───────────────┘└───────────────┘└──────────┘└──────
582      rwa [← int.dvd_nat_abs, int.coe_nat_dvd, ← int.dvd_nat_abs, int.coe_nat_dvd]⟩,
id              └─────────────┘  └─────────────┘    └─────────────┘  └─────────────┘
src      └─────┘└─────────────┘└┘└─────────────┘└──┘└─────────────┘└┘└─────────────┘
typ      └─────┘└─────────────┘└┘└─────────────┘└──┘└─────────────┘└┘└─────────────┘
doc      └─────┘               └┘               └──┘               └┘               
txt      └─────┘               └┘               └──┘               └┘               
par      └─────┘               └┘               └──┘               └┘               
pid         └──┘               └┘               └──┘               └┘               
st   ────────┘└───────────────┘└───────────────┘└─────────────────┘└───────────────┘
583    λ hp, nat.prime_iff_prime.2 ⟨int.coe_nat_ne_zero.1 hp.1,
id       └┘  └─────────────────┘   └─────────────────┘  └┘
src          └─────────────────┘   └─────────────────┘    
typ      └┘  └─────────────────┘   └─────────────────┘  └┘
584        mt is_unit_nat.1 $ λ h, by simpa [h, not_prime_one] using hp,
id         └┘ └─────────┘                    └───────────┘        └┘
src        └┘ └─────────┘            └─────┘ └┘└───────────┘└──────┘
typ        └┘ └─────────┘           └─────┘└┘└───────────┘└──────┘└┘
doc                                   └─────┘ └┘             └──────┘
txt                                   └─────┘ └┘             └──────┘
par                                   └─────┘ └┘             └──────┘
pid                                         └┘             └────┘
st                                   └────────────────────────────────┘
585      λ a b, by simpa only [int.coe_nat_dvd, (int.coe_nat_mul _ _).symm] using hp.2.2 a b⟩⟩
id                           └─────────────┘   └─────────────┘                  └┘      
src                └──────────┘└─────────────┘└┘ └─────────────┘└────────────────┘  └───┘ 
typ              └──────────┘└─────────────┘└┘ └─────────────┘└────────────────┘└┘└───┘
doc                └──────────┘               └┘                └────────────────┘  └───┘ 
txt                └──────────┘               └┘                └────────────────┘  └───┘ 
par                └──────────┘               └┘                └────────────────┘  └───┘ 
pid                     └──┘└┘               └┘                └─────────┘└────┘  └───┘ 
st                └────────────────────────────────────────────────────────────────────────┘
586  
587  def associates_int_equiv_nat : associates ℤ ≃ ℕ :=
id                                  └────────┘   
src                                 └────────┘   
typ                                 └────────┘   
doc                                              
588  begin
st   └─────
589    refine ⟨λz, z.out.nat_abs, λn, associates.mk n, _, _⟩,
id                  └──┘└──────┘      └───────────┘
src    └─────┘  └─┘ └──┘└──────┘└┘ └─┘└───────────┘ └─────┘
typ    └─────┘  └─┘ └──┘└──────┘└┘ └─┘└───────────┘ └─────┘
doc    └─────┘  └─┘             └┘ └─┘              └─────┘
txt    └─────┘  └─┘             └┘ └─┘              └─────┘
par    └─────┘  └─┘             └┘ └─┘              └─────┘
pid            └─┘             └┘ └─┘              └─────┘
st   ──────────────────────────────────────────────────────┘└─
590    { refine (assume a, quotient.induction_on' a $ assume a,
id                         └────────────────────┘
src      └─────┘       └──┘└────────────────────┘        └───
typ      └─────┘       └──┘└────────────────────┘        └───
doc      └─────┘       └──┘                              └───
txt      └─────┘       └──┘                              └───
par      └─────┘       └──┘                              └───
pid                   └──┘                              └───
st   ───┘└──────────────────────────────────────────────────────
591        associates.mk_eq_mk_iff_associated.2 $ associated.symm $ ⟨norm_unit a, _⟩),
id         └────────────────────────────────┘     └─────────────┘    └───────┘
src  ─────┘└────────────────────────────────┘└─┘ └─────────────┘  └───────┘ └───┘
typ  ─────┘└────────────────────────────────┘└─┘ └─────────────┘  └───────┘ └───┘
doc  ─────┘                                  └─┘                            └───┘
txt  ─────┘                                  └─┘                            └───┘
par  ─────┘                                  └─┘                            └───┘
pid  ─────┘                                  └─┘                            └───┘
st   ───────────────────────────────────────────────────────────────────────────────┘└─
592      show normalize a = int.nat_abs (normalize a),
id                         └─────────┘  └───────┘ 
src      └───┘          └─────────┘ └───────┘ 
typ      └───┘          └─────────┘ └───────┘
doc      └───┘                                 
txt      └───┘                                 
par      └───┘                                 
pid      └───┘                                 
st   ───────────────────────────────────────────────┘└─
593      rw [int.coe_nat_abs_eq_normalize, normalize_idem] },
id           └──────────────────────────┘  └────────────┘
src      └──┘└──────────────────────────┘└┘└────────────┘└┘
typ      └──┘└──────────────────────────┘└┘└────────────┘└┘
doc      └──┘                            └┘              └┘
txt      └──┘                            └┘              └┘
par      └──┘                            └┘              └┘
pid        └┘                            └┘              
st   ───────────────────────────────────┘└──────────────┘└┘
594    { assume n, show int.nat_abs (normalize n) = n,
id                      └─────────┘  └───────┘      
src      └──────┘  └───┘└─────────┘ └───────┘ └┘ 
typ      └──────┘  └───┘└─────────┘ └───────┘ └┘ 
doc      └──────┘  └───┘                      └┘ 
txt      └──────┘  └───┘                      └┘ 
par      └──────┘  └───┘                      └┘ 
pid      └──────┘  └───┘                      └┘ 
st   ───────────┘└──────────────────────────────────┘└─
595      rw [← int.coe_nat_abs_eq_normalize, int.nat_abs_of_nat, int.nat_abs_of_nat] }
id             └──────────────────────────┘  └────────────────┘  └────────────────┘
src      └────┘└──────────────────────────┘└┘└────────────────┘└┘└────────────────┘└┘
typ      └────┘└──────────────────────────┘└┘└────────────────┘└┘└────────────────┘└┘
doc      └────┘                            └┘                  └┘                  └┘
txt      └────┘                            └┘                  └┘                  └┘
par      └────┘                            └┘                  └┘                  └┘
pid        └──┘                            └┘                  └┘                  
st   ─────────────────────────────────────┘└──────────────────┘└──────────────────┘└─
596  end
st   ──┘